N-ary images of sets #
This file defines Set.image2, the binary image of finsets. This is the finset version of
set.image2. This is mostly useful to define pointwise operations.
Notes #
This file is very similar to the n-ary section of Data.Set.Basic, to Order.Filter.NAry and to
Data.Option.NAry. Please keep them in sync.
We do not define Set.image3 as its only purpose would be to prove properties of Set.image2
and Set.image2 already fulfills this task.
theorem
Set.mem_image2_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{a : α}
{b : β}
(hf : Function.Injective2 f)
:
theorem
Set.image2_subset
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{s : Set α}
{s' : Set α}
{t : Set β}
{t' : Set β}
(hs : s ⊆ s')
(ht : t ⊆ t')
:
Set.image2 f s t ⊆ Set.image2 f s' t'
image2 is monotone with respect to ⊆.
theorem
Set.image2_subset_left
{α : Type u_3}
{β : Type u_1}
{γ : Type u_2}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{t' : Set β}
(ht : t ⊆ t')
:
Set.image2 f s t ⊆ Set.image2 f s t'
theorem
Set.image2_subset_right
{α : Type u_1}
{β : Type u_3}
{γ : Type u_2}
{f : α → β → γ}
{s : Set α}
{s' : Set α}
{t : Set β}
(hs : s ⊆ s')
:
Set.image2 f s t ⊆ Set.image2 f s' t
@[simp]
theorem
Set.image_uncurry_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(s : Set α)
(t : Set β)
:
Function.uncurry f '' s ×ˢ t = Set.image2 f s t
@[simp]
theorem
Set.image2_mk_eq_prod
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
:
Set.image2 Prod.mk s t = s ×ˢ t
theorem
Set.image2_union_left
{α : Type u_2}
{β : Type u_3}
{γ : Type u_1}
{f : α → β → γ}
{s : Set α}
{s' : Set α}
{t : Set β}
:
Set.image2 f (s ∪ s') t = Set.image2 f s t ∪ Set.image2 f s' t
theorem
Set.image2_union_right
{α : Type u_2}
{β : Type u_3}
{γ : Type u_1}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{t' : Set β}
:
Set.image2 f s (t ∪ t') = Set.image2 f s t ∪ Set.image2 f s t'
theorem
Set.image2_inter_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{s : Set α}
{s' : Set α}
{t : Set β}
(hf : Function.Injective2 f)
:
Set.image2 f (s ∩ s') t = Set.image2 f s t ∩ Set.image2 f s' t
theorem
Set.image2_inter_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{t' : Set β}
(hf : Function.Injective2 f)
:
Set.image2 f s (t ∩ t') = Set.image2 f s t ∩ Set.image2 f s t'
theorem
Set.Nonempty.image2
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{s : Set α}
{t : Set β}
:
Set.Nonempty s → Set.Nonempty t → Set.Nonempty (Set.image2 f s t)
@[simp]
theorem
Set.image2_nonempty_iff
{α : Type u_2}
{β : Type u_3}
{γ : Type u_1}
{f : α → β → γ}
{s : Set α}
{t : Set β}
:
Set.Nonempty (Set.image2 f s t) ↔ Set.Nonempty s ∧ Set.Nonempty t
theorem
Set.Nonempty.of_image2_left
{α : Type u_2}
{β : Type u_3}
{γ : Type u_1}
{f : α → β → γ}
{s : Set α}
{t : Set β}
(h : Set.Nonempty (Set.image2 f s t))
:
theorem
Set.Nonempty.of_image2_right
{α : Type u_2}
{β : Type u_3}
{γ : Type u_1}
{f : α → β → γ}
{s : Set α}
{t : Set β}
(h : Set.Nonempty (Set.image2 f s t))
:
theorem
Set.image2_inter_subset_left
{α : Type u_2}
{β : Type u_3}
{γ : Type u_1}
{f : α → β → γ}
{s : Set α}
{s' : Set α}
{t : Set β}
:
Set.image2 f (s ∩ s') t ⊆ Set.image2 f s t ∩ Set.image2 f s' t
theorem
Set.image2_inter_subset_right
{α : Type u_2}
{β : Type u_3}
{γ : Type u_1}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{t' : Set β}
:
Set.image2 f s (t ∩ t') ⊆ Set.image2 f s t ∩ Set.image2 f s t'
@[simp]
theorem
Set.image2_singleton_left
{α : Type u_2}
{β : Type u_3}
{γ : Type u_1}
{f : α → β → γ}
{t : Set β}
{a : α}
:
Set.image2 f {a} t = f a '' t
@[simp]
theorem
Set.image2_singleton_right
{α : Type u_2}
{β : Type u_3}
{γ : Type u_1}
{f : α → β → γ}
{s : Set α}
{b : β}
:
Set.image2 f s {b} = (fun a => f a b) '' s
theorem
Set.image2_singleton
{α : Type u_2}
{β : Type u_3}
{γ : Type u_1}
{f : α → β → γ}
{a : α}
{b : β}
:
Set.image2 f {a} {b} = {f a b}
theorem
Set.image2_congr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{f' : α → β → γ}
{s : Set α}
{t : Set β}
(h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → f a b = f' a b)
:
Set.image2 f s t = Set.image2 f' s t
theorem
Set.image2_congr'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_1}
{f : α → β → γ}
{f' : α → β → γ}
{s : Set α}
{t : Set β}
(h : ∀ (a : α) (b : β), f a b = f' a b)
:
Set.image2 f s t = Set.image2 f' s t
A common special case of image2_congr
def
Set.image3
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
(g : α → β → γ → δ)
(s : Set α)
(t : Set β)
(u : Set γ)
:
Set δ
The image of a ternary function f : α → β → γ → δ as a function
Set α → Set β → Set γ → Set δ. Mathematically this should be thought of as the image of the
corresponding function α × β × γ → δ.
theorem
Set.image3_congr'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{δ : Type u_1}
{g : α → β → γ → δ}
{g' : α → β → γ → δ}
{s : Set α}
{t : Set β}
{u : Set γ}
(h : ∀ (a : α) (b : β) (c : γ), g a b c = g' a b c)
:
Set.image3 g s t u = Set.image3 g' s t u
A common special case of image3_congr
theorem
Set.image2_image2_left
{α : Type u_4}
{β : Type u_5}
{γ : Type u_3}
{δ : Type u_2}
{ε : Type u_1}
{s : Set α}
{t : Set β}
{u : Set γ}
(f : δ → γ → ε)
(g : α → β → δ)
:
Set.image2 f (Set.image2 g s t) u = Set.image3 (fun a b c => f (g a b) c) s t u
theorem
Set.image2_image2_right
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
{δ : Type u_3}
{ε : Type u_1}
{s : Set α}
{t : Set β}
{u : Set γ}
(f : α → δ → ε)
(g : β → γ → δ)
:
Set.image2 f s (Set.image2 g t u) = Set.image3 (fun a b c => f a (g b c)) s t u
theorem
Set.image_image2
{α : Type u_3}
{β : Type u_4}
{γ : Type u_2}
{δ : Type u_1}
{s : Set α}
{t : Set β}
(f : α → β → γ)
(g : γ → δ)
:
g '' Set.image2 f s t = Set.image2 (fun a b => g (f a b)) s t
theorem
Set.image2_image_left
{α : Type u_4}
{β : Type u_3}
{γ : Type u_2}
{δ : Type u_1}
{s : Set α}
{t : Set β}
(f : γ → β → δ)
(g : α → γ)
:
Set.image2 f (g '' s) t = Set.image2 (fun a b => f (g a) b) s t
theorem
Set.image2_image_right
{α : Type u_2}
{β : Type u_4}
{γ : Type u_3}
{δ : Type u_1}
{s : Set α}
{t : Set β}
(f : α → γ → δ)
(g : β → γ)
:
Set.image2 f s (g '' t) = Set.image2 (fun a b => f a (g b)) s t
theorem
Set.image2_swap
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(s : Set α)
(t : Set β)
:
Set.image2 f s t = Set.image2 (fun a b => f b a) t s
@[simp]
theorem
Set.image2_left
{α : Type u_2}
{β : Type u_1}
{s : Set α}
{t : Set β}
(h : Set.Nonempty t)
:
Set.image2 (fun x x_1 => x) s t = s
@[simp]
theorem
Set.image2_right
{α : Type u_1}
{β : Type u_2}
{s : Set α}
{t : Set β}
(h : Set.Nonempty s)
:
Set.image2 (fun x y => y) s t = t
theorem
Set.image2_assoc
{α : Type u_4}
{β : Type u_5}
{γ : Type u_3}
{δ : Type u_2}
{ε : Type u_1}
{ε' : Type u_6}
{s : Set α}
{t : Set β}
{u : Set γ}
{f : δ → γ → ε}
{g : α → β → δ}
{f' : α → ε' → ε}
{g' : β → γ → ε'}
(h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c))
:
Set.image2 f (Set.image2 g s t) u = Set.image2 f' s (Set.image2 g' t u)
theorem
Set.image2_comm
{α : Type u_2}
{β : Type u_3}
{γ : Type u_1}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{g : β → α → γ}
(h_comm : ∀ (a : α) (b : β), f a b = g b a)
:
Set.image2 f s t = Set.image2 g t s
theorem
Set.image2_left_comm
{α : Type u_2}
{β : Type u_4}
{γ : Type u_5}
{δ : Type u_3}
{δ' : Type u_6}
{ε : Type u_1}
{s : Set α}
{t : Set β}
{u : Set γ}
{f : α → δ → ε}
{g : β → γ → δ}
{f' : α → γ → δ'}
{g' : β → δ' → ε}
(h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c))
:
Set.image2 f s (Set.image2 g t u) = Set.image2 g' t (Set.image2 f' s u)
theorem
Set.image2_right_comm
{α : Type u_4}
{β : Type u_5}
{γ : Type u_3}
{δ : Type u_2}
{δ' : Type u_6}
{ε : Type u_1}
{s : Set α}
{t : Set β}
{u : Set γ}
{f : δ → γ → ε}
{g : α → β → δ}
{f' : α → γ → δ'}
{g' : δ' → β → ε}
(h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b)
:
Set.image2 f (Set.image2 g s t) u = Set.image2 g' (Set.image2 f' s u) t
theorem
Set.image2_image2_image2_comm
{α : Type u_4}
{β : Type u_5}
{γ : Type u_6}
{δ : Type u_7}
{ε : Type u_2}
{ε' : Type u_8}
{ζ : Type u_3}
{ζ' : Type u_9}
{ν : Type u_1}
{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))
:
Set.image2 f (Set.image2 g s t) (Set.image2 h u v) = Set.image2 f' (Set.image2 g' s u) (Set.image2 h' t v)
theorem
Set.image_image2_distrib
{α : Type u_3}
{α' : Type u_5}
{β : Type u_4}
{β' : Type u_6}
{γ : Type u_2}
{δ : Type u_1}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{g : γ → δ}
{f' : α' → β' → δ}
{g₁ : α → α'}
{g₂ : β → β'}
(h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b))
:
g '' Set.image2 f s t = Set.image2 f' (g₁ '' s) (g₂ '' t)
theorem
Set.image_image2_distrib_left
{α : Type u_3}
{α' : Type u_5}
{β : Type u_4}
{γ : Type u_2}
{δ : Type u_1}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{g : γ → δ}
{f' : α' → β → δ}
{g' : α → α'}
(h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b)
:
g '' Set.image2 f s t = Set.image2 f' (g' '' s) t
Symmetric statement to Set.image2_image_left_comm.
theorem
Set.image_image2_distrib_right
{α : Type u_3}
{β : Type u_4}
{β' : Type u_5}
{γ : Type u_2}
{δ : Type u_1}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{g : γ → δ}
{f' : α → β' → δ}
{g' : β → β'}
(h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b))
:
g '' Set.image2 f s t = Set.image2 f' s (g' '' t)
Symmetric statement to Set.image_image2_right_comm.
theorem
Set.image2_image_left_comm
{α : Type u_4}
{α' : Type u_2}
{β : Type u_3}
{γ : Type u_1}
{δ : Type u_5}
{s : Set α}
{t : Set β}
{f : α' → β → γ}
{g : α → α'}
{f' : α → β → δ}
{g' : δ → γ}
(h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b))
:
Set.image2 f (g '' s) t = g' '' Set.image2 f' s t
Symmetric statement to Set.image_image2_distrib_left.
theorem
Set.image_image2_right_comm
{α : Type u_2}
{β : Type u_4}
{β' : Type u_3}
{γ : Type u_1}
{δ : Type u_5}
{s : Set α}
{t : Set β}
{f : α → β' → γ}
{g : β → β'}
{f' : α → β → δ}
{g' : δ → γ}
(h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b))
:
Set.image2 f s (g '' t) = g' '' Set.image2 f' s t
Symmetric statement to Set.image_image2_distrib_right.
theorem
Set.image2_distrib_subset_left
{α : Type u_2}
{β : Type u_4}
{β' : Type u_6}
{γ : Type u_5}
{γ' : Type u_7}
{δ : Type u_3}
{ε : Type u_1}
{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))
:
Set.image2 f s (Set.image2 g t u) ⊆ Set.image2 g' (Set.image2 f₁ s t) (Set.image2 f₂ s u)
The other direction does not hold because of the s-s cross terms on the RHS.
theorem
Set.image2_distrib_subset_right
{α : Type u_4}
{α' : Type u_6}
{β : Type u_5}
{β' : Type u_7}
{γ : Type u_3}
{δ : Type u_2}
{ε : Type u_1}
{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))
:
Set.image2 f (Set.image2 g s t) u ⊆ Set.image2 g' (Set.image2 f₁ s u) (Set.image2 f₂ t u)
The other direction does not hold because of the u-u cross terms on the RHS.
theorem
Set.image_image2_antidistrib
{α : Type u_3}
{α' : Type u_6}
{β : Type u_4}
{β' : Type u_5}
{γ : Type u_2}
{δ : Type u_1}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{g : γ → δ}
{f' : β' → α' → δ}
{g₁ : β → β'}
{g₂ : α → α'}
(h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a))
:
g '' Set.image2 f s t = Set.image2 f' (g₁ '' t) (g₂ '' s)
theorem
Set.image_image2_antidistrib_left
{α : Type u_3}
{β : Type u_4}
{β' : Type u_5}
{γ : Type u_2}
{δ : Type u_1}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{g : γ → δ}
{f' : β' → α → δ}
{g' : β → β'}
(h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a)
:
g '' Set.image2 f s t = Set.image2 f' (g' '' t) s
Symmetric statement to Set.image2_image_left_anticomm.
theorem
Set.image_image2_antidistrib_right
{α : Type u_3}
{α' : Type u_5}
{β : Type u_4}
{γ : Type u_2}
{δ : Type u_1}
{f : α → β → γ}
{s : Set α}
{t : Set β}
{g : γ → δ}
{f' : β → α' → δ}
{g' : α → α'}
(h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a))
:
g '' Set.image2 f s t = Set.image2 f' t (g' '' s)
Symmetric statement to Set.image_image2_right_anticomm.
theorem
Set.image2_image_left_anticomm
{α : Type u_4}
{α' : Type u_2}
{β : Type u_3}
{γ : Type u_1}
{δ : Type u_5}
{s : Set α}
{t : Set β}
{f : α' → β → γ}
{g : α → α'}
{f' : β → α → δ}
{g' : δ → γ}
(h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a))
:
Set.image2 f (g '' s) t = g' '' Set.image2 f' t s
Symmetric statement to Set.image_image2_antidistrib_left.
theorem
Set.image_image2_right_anticomm
{α : Type u_2}
{β : Type u_4}
{β' : Type u_3}
{γ : Type u_1}
{δ : Type u_5}
{s : Set α}
{t : Set β}
{f : α → β' → γ}
{g : β → β'}
{f' : β → α → δ}
{g' : δ → γ}
(h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a))
:
Set.image2 f s (g '' t) = g' '' Set.image2 f' t s
Symmetric statement to Set.image_image2_antidistrib_right.
theorem
Set.image2_left_identity
{α : Type u_2}
{β : Type u_1}
{f : α → β → β}
{a : α}
(h : ∀ (b : β), f a b = b)
(t : Set β)
:
Set.image2 f {a} t = t
If a is a left identity for f : α → β → β, then {a} is a left identity for
Set.image2 f.
theorem
Set.image2_right_identity
{α : Type u_1}
{β : Type u_2}
{f : α → β → α}
{b : β}
(h : ∀ (a : α), f a b = a)
(s : Set α)
:
Set.image2 f s {b} = s
If b is a right identity for f : α → β → α, then {b} is a right identity for
Set.image2 f.
theorem
Set.image2_inter_union_subset
{α : Type u_1}
{β : Type u_2}
{f : α → α → β}
{s : Set α}
{t : Set α}
(hf : ∀ (a b : α), f a b = f b a)
:
Set.image2 f (s ∩ t) (s ∪ t) ⊆ Set.image2 f s t
theorem
Set.image2_union_inter_subset
{α : Type u_1}
{β : Type u_2}
{f : α → α → β}
{s : Set α}
{t : Set α}
(hf : ∀ (a b : α), f a b = f b a)
:
Set.image2 f (s ∪ t) (s ∩ t) ⊆ Set.image2 f s t