N-ary images of sets #
This file defines Set.image2, the binary image of sets.
This is mostly useful to define pointwise operations and Set.seq.
Notes #
This file is very similar to Data.Finset.NAry, to Order.Filter.NAry, and to
Data.Option.NAry. Please keep them in sync.
theorem
Set.Nonempty.of_image2_left
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : Set α}
{t : Set β}
(h : (Set.image2 f s t).Nonempty)
:
s.Nonempty
theorem
Set.Nonempty.of_image2_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{f : α → β → γ}
{s : Set α}
{t : Set β}
(h : (Set.image2 f s t).Nonempty)
:
t.Nonempty
theorem
Set.Subsingleton.image2
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{s : Set α}
{t : Set β}
(hs : s.Subsingleton)
(ht : t.Subsingleton)
(f : α → β → γ)
:
(Set.image2 f s t).Subsingleton
theorem
Set.image2_image2_image2_comm
{α : Type u_1}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{ε : Type u_9}
{ε' : Type u_10}
{ζ : Type u_11}
{ζ' : Type u_12}
{ν : Type u_13}
{s : Set α}
{t : Set β}
{u : Set γ}
{v : Set δ}
{f : ε → ζ → ν}
{g : α → β → ε}
{h : γ → δ → ζ}
{f' : ε' → ζ' → ν}
{g' : α → γ → ε'}
{h' : β → δ → ζ'}
(h_comm : ∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d))
:
theorem
Set.image_image2_distrib_left
{α : Type u_1}
{α' : Type u_2}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{g : γ → δ}
{f' : α' → β → δ}
{g' : α → α'}
(h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b)
:
Symmetric statement to Set.image2_image_left_comm.
theorem
Set.image_image2_distrib_right
{α : Type u_1}
{β : Type u_3}
{β' : Type u_4}
{γ : Type u_5}
{δ : Type u_7}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{g : γ → δ}
{f' : α → β' → δ}
{g' : β → β'}
(h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b))
:
Symmetric statement to Set.image_image2_right_comm.
theorem
Set.image2_image_left_comm
{α : Type u_1}
{α' : Type u_2}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{s : Set α}
{t : Set β}
{f : α' → β → γ}
{g : α → α'}
{f' : α → β → δ}
{g' : δ → γ}
(h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b))
:
Symmetric statement to Set.image_image2_distrib_left.
theorem
Set.image_image2_right_comm
{α : Type u_1}
{β : Type u_3}
{β' : Type u_4}
{γ : Type u_5}
{δ : Type u_7}
{s : Set α}
{t : Set β}
{f : α → β' → γ}
{g : β → β'}
{f' : α → β → δ}
{g' : δ → γ}
(h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b))
:
Symmetric statement to Set.image_image2_distrib_right.
theorem
Set.image2_distrib_subset_left
{α : Type u_1}
{β : Type u_3}
{β' : Type u_4}
{γ : Type u_5}
{γ' : Type u_6}
{δ : Type u_7}
{ε : Type u_9}
{s : Set α}
{t : Set β}
{u : Set γ}
{f : α → δ → ε}
{g : β → γ → δ}
{f₁ : α → β → β'}
{f₂ : α → γ → γ'}
{g' : β' → γ' → ε}
(h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c))
:
The other direction does not hold because of the s-s cross terms on the RHS.
theorem
Set.image2_distrib_subset_right
{α : Type u_1}
{α' : Type u_2}
{β : Type u_3}
{β' : Type u_4}
{γ : Type u_5}
{δ : Type u_7}
{ε : Type u_9}
{s : Set α}
{t : Set β}
{u : Set γ}
{f : δ → γ → ε}
{g : α → β → δ}
{f₁ : α → γ → α'}
{f₂ : β → γ → β'}
{g' : α' → β' → ε}
(h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c))
:
The other direction does not hold because of the u-u cross terms on the RHS.
theorem
Set.image_image2_antidistrib_left
{α : Type u_1}
{β : Type u_3}
{β' : Type u_4}
{γ : Type u_5}
{δ : Type u_7}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{g : γ → δ}
{f' : β' → α → δ}
{g' : β → β'}
(h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a)
:
Symmetric statement to Set.image2_image_left_anticomm.
theorem
Set.image_image2_antidistrib_right
{α : Type u_1}
{α' : Type u_2}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{g : γ → δ}
{f' : β → α' → δ}
{g' : α → α'}
(h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a))
:
Symmetric statement to Set.image_image2_right_anticomm.
theorem
Set.image2_image_left_anticomm
{α : Type u_1}
{α' : Type u_2}
{β : Type u_3}
{γ : Type u_5}
{δ : Type u_7}
{s : Set α}
{t : Set β}
{f : α' → β → γ}
{g : α → α'}
{f' : β → α → δ}
{g' : δ → γ}
(h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a))
:
Symmetric statement to Set.image_image2_antidistrib_left.
theorem
Set.image_image2_right_anticomm
{α : Type u_1}
{β : Type u_3}
{β' : Type u_4}
{γ : Type u_5}
{δ : Type u_7}
{s : Set α}
{t : Set β}
{f : α → β' → γ}
{g : β → β'}
{f' : β → α → δ}
{g' : δ → γ}
(h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a))
:
Symmetric statement to Set.image_image2_antidistrib_right.