# Documentation

Mathlib.Data.Set.NAry

# 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.

def Set.image2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (s : Set α) (t : Set β) :
Set γ

The image of a binary function f : α → β → γ as a function Set α → Set β → Set γ. Mathematically this should be thought of as the image of the corresponding function α × β → γ.

Equations
@[simp]
theorem Set.mem_image2 {α : Type u_2} {β : Type u_3} {γ : Type u_1} {f : αβγ} {s : Set α} {t : Set β} {c : γ} :
c Set.image2 f s t a b, a s b t f a b = c
theorem Set.mem_image2_of_mem {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (ha : a s) (hb : b t) :
f a b Set.image2 f s t
theorem Set.mem_image2_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (hf : ) :
f a b Set.image2 f s t a s b t
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') :
theorem Set.image2_subset_right {α : Type u_1} {β : Type u_3} {γ : Type u_2} {f : αβγ} {s : Set α} {s' : Set α} {t : Set β} (hs : s s') :
theorem Set.image_subset_image2_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} {f : αβγ} {s : Set α} {t : Set β} {b : β} (hb : b t) :
(fun a => f a b) '' s Set.image2 f s t
theorem Set.image_subset_image2_right {α : Type u_1} {β : Type u_3} {γ : Type u_2} {f : αβγ} {s : Set α} {t : Set β} {a : α} (ha : a s) :
f a '' t Set.image2 f s t
theorem Set.forall_image2_iff {α : Type u_2} {β : Type u_3} {γ : Type u_1} {f : αβγ} {s : Set α} {t : Set β} {p : γProp} :
((z : γ) → z Set.image2 f s tp z) (x : α) → x s(y : β) → y tp (f x y)
@[simp]
theorem Set.image2_subset_iff {α : Type u_2} {β : Type u_3} {γ : Type u_1} {f : αβγ} {s : Set α} {t : Set β} {u : Set γ} :
Set.image2 f s t u ∀ (x : α), x s∀ (y : β), y tf x y u
theorem Set.image_prod {α : Type u_2} {β : Type u_3} {γ : Type u_1} (f : αβγ) {s : Set α} {t : Set β} :
(fun x => f x.fst x.snd) '' 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 β) :
'' 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_curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α × βγ) (s : Set α) (t : Set β) :
Set.image2 (fun a b => f (a, b)) s t = f '' 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 : ) :
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 : ) :
Set.image2 f s (t t') = Set.image2 f s t Set.image2 f s t'
@[simp]
theorem Set.image2_empty_left {α : Type u_2} {β : Type u_3} {γ : Type u_1} {f : αβγ} {t : Set β} :
@[simp]
theorem Set.image2_empty_right {α : Type u_2} {β : Type u_3} {γ : Type u_1} {f : αβγ} {s : Set α} :
theorem Set.Nonempty.image2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {s : Set α} {t : Set β} :
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 β} :
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)) :
@[simp]
theorem Set.image2_eq_empty_iff {α : Type u_2} {β : Type u_3} {γ : Type u_1} {f : αβγ} {s : Set α} {t : Set β} :
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 tf 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 α × β × γ → δ.

Equations
@[simp]
theorem Set.mem_image3 {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_1} {g : αβγδ} {s : Set α} {t : Set β} {u : Set γ} {d : δ} :
d Set.image3 g s t u a b c, a s b t c u g a b c = d
theorem Set.image3_mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {g : αβγδ} {s : Set α} {s' : Set α} {t : Set β} {t' : Set β} {u : Set γ} {u' : Set γ} (hs : s s') (ht : t t') (hu : u u') :
Set.image3 g s t u Set.image3 g s' t' u'
theorem Set.image3_congr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {g : αβγδ} {g' : αβγδ} {s : Set α} {t : Set β} {u : Set γ} (h : ∀ (a : α), a s∀ (b : β), b t∀ (c : γ), c ug a b c = g' a b c) :
Set.image3 g s t u = Set.image3 g' s t u
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.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.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