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

source
theorem Set.mem_image2_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (hf : Function.Injective2 f) :
f a b ∈ image2 f s t ↔ a ∈ s ∧ b ∈ t
source
theorem Set.image2_subset {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t t' : Set β} (hs : s ⊆ s') (ht : t ⊆ t') :
image2 f s t ⊆ image2 f s' t'

image2 is monotone with respect to `⊆`.

source
theorem Set.image2_subset_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t t' : Set β} (ht : t ⊆ t') :
image2 f s t ⊆ image2 f s t'
source
theorem Set.image2_subset_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t : Set β} (hs : s ⊆ s') :
image2 f s t ⊆ image2 f s' t
source
theorem Set.image_subset_image2_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {b : β} (hb : b ∈ t) :
(fun (a : α) => f a b) '' s ⊆ image2 f s t
source
theorem Set.image_subset_image2_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {a : α} (ha : a ∈ s) :
f a '' t ⊆ image2 f s t
source
theorem Set.forall_mem_image2 {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {p : γ → Prop} :
(∀ z ∈ image2 f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)
source
theorem Set.exists_mem_image2 {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {p : γ → Prop} :
(∃ z ∈ image2 f s t, p z) ↔ ∃ x ∈ s, ∃ y ∈ t, p (f x y)
source
@[simp]
theorem Set.image2_subset_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {u : Set γ} :
image2 f s t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u
source
theorem Set.image2_subset_iff_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {u : Set γ} :
image2 f s t ⊆ u ↔ ∀ a ∈ s, (fun (b : β) => f a b) '' t ⊆ u
source
theorem Set.image2_subset_iff_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {u : Set γ} :
image2 f s t ⊆ u ↔ ∀ b ∈ t, (fun (a : α) => f a b) '' s ⊆ u
source
@[simp]
theorem Set.image_prod {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α → β → γ) {s : Set α} {t : Set β} :
(fun (x : α × β) => f x.1 x.2) '' s ×ˢ t = image2 f s t
source
@[simp]
theorem Set.image_uncurry_prod {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α → β → γ) (s : Set α) (t : Set β) :
Function.uncurry f '' s ×ˢ t = image2 f s t
source
@[simp]
theorem Set.image2_mk_eq_prod {α : Type u_1} {β : Type u_3} {s : Set α} {t : Set β} :
image2 Prod.mk s t = s ×ˢ t
source
@[simp]
theorem Set.image2_curry {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α × β → γ) (s : Set α) (t : Set β) :
image2 (fun (a : α) (b : β) => f (a, b)) s t = f '' s ×ˢ t
source
theorem Set.image2_swap {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α → β → γ) (s : Set α) (t : Set β) :
image2 f s t = image2 (fun (a : β) (b : α) => f b a) t s
source
theorem Set.image2_union_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t : Set β} :
image2 f (s ∪ s') t = image2 f s t ∪ image2 f s' t
source
theorem Set.image2_union_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t t' : Set β} :
image2 f s (t ∪ t') = image2 f s t ∪ image2 f s t'
source
theorem Set.image2_inter_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t : Set β} (hf : Function.Injective2 f) :
image2 f (s ∩ s') t = image2 f s t ∩ image2 f s' t
source
theorem Set.image2_inter_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t t' : Set β} (hf : Function.Injective2 f) :
image2 f s (t ∩ t') = image2 f s t ∩ image2 f s t'
source
@[simp]
theorem Set.image2_empty_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {t : Set β} :
image2 f ∅ t = ∅
source
@[simp]
theorem Set.image2_empty_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} :
image2 f s ∅ = ∅
source
theorem Set.Nonempty.image2 {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} :
s.Nonempty → t.Nonempty → (Set.image2 f s t).Nonempty
source
@[simp]
theorem Set.image2_nonempty_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} :
(image2 f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
source
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
source
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
source
@[simp]
theorem Set.image2_eq_empty_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} :
image2 f s t = ∅ ↔ s = ∅ ∨ t = ∅
source
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
source
theorem Set.image2_inter_subset_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t : Set β} :
image2 f (s ∩ s') t ⊆ image2 f s t ∩ image2 f s' t
source
theorem Set.image2_inter_subset_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t t' : Set β} :
image2 f s (t ∩ t') ⊆ image2 f s t ∩ image2 f s t'
source
@[simp]
theorem Set.image2_singleton_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {t : Set β} {a : α} :
image2 f {a} t = f a '' t
source
@[simp]
theorem Set.image2_singleton_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {b : β} :
image2 f s {b} = (fun (a : α) => f a b) '' s
source
theorem Set.image2_singleton {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {a : α} {b : β} :
image2 f {a} {b} = {f a b}
source
@[simp]
theorem Set.image2_insert_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {a : α} :
image2 f (insert a s) t = (fun (b : β) => f a b) '' t ∪ image2 f s t
source
@[simp]
theorem Set.image2_insert_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {b : β} :
image2 f s (insert b t) = (fun (a : α) => f a b) '' s ∪ image2 f s t
source
theorem Set.image2_congr {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f f' : α → β → γ} {s : Set α} {t : Set β} (h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b) :
image2 f s t = image2 f' s t
source
theorem Set.image2_congr' {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f f' : α → β → γ} {s : Set α} {t : Set β} (h : ∀ (a : α) (b : β), f a b = f' a b) :
image2 f s t = image2 f' s t

A common special case of `image2_congr`

source
theorem Set.image_image2 {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β} (f : α → β → γ) (g : γ → δ) :
g '' image2 f s t = image2 (fun (a : α) (b : β) => g (f a b)) s t
source
theorem Set.image2_image_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β} (f : γ → β → δ) (g : α → γ) :
image2 f (g '' s) t = image2 (fun (a : α) (b : β) => f (g a) b) s t
source
theorem Set.image2_image_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β} (f : α → γ → δ) (g : β → γ) :
image2 f s (g '' t) = image2 (fun (a : α) (b : β) => f a (g b)) s t
source
@[simp]
theorem Set.image2_left {α : Type u_1} {β : Type u_3} {s : Set α} {t : Set β} (h : t.Nonempty) :
image2 (fun (x : α) (x_1 : β) => x) s t = s
source
@[simp]
theorem Set.image2_right {α : Type u_1} {β : Type u_3} {s : Set α} {t : Set β} (h : s.Nonempty) :
image2 (fun (x : α) (y : β) => y) s t = t
source
theorem Set.image2_range {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} (f : α' → β' → γ) (g : α → α') (h : β → β') :
image2 f (range g) (range h) = range fun (x : α × β) => f (g x.1) (h x.2)
source
theorem Set.image2_assoc {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {ε' : Type u_10} {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)) :
image2 f (image2 g s t) u = image2 f' s (image2 g' t u)
source
theorem Set.image2_comm {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {g : β → α → γ} (h_comm : ∀ (a : α) (b : β), f a b = g b a) :
image2 f s t = image2 g t s
source
theorem Set.image2_left_comm {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} {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)) :
image2 f s (image2 g t u) = image2 g' t (image2 f' s u)
source
theorem Set.image2_right_comm {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} {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) :
image2 f (image2 g s t) u = image2 g' (image2 f' s u) t
source
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)) :
image2 f (image2 g s t) (image2 h u v) = image2 f' (image2 g' s u) (image2 h' t v)
source
theorem Set.image_image2_distrib {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ} {s : Set α} {t : Set β} {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'} (h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)) :
g '' image2 f s t = image2 f' (g₁ '' s) (g₂ '' t)
source
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) :
g '' image2 f s t = image2 f' (g' '' s) t

Symmetric statement to `Set.image2_image_left_comm`.

source
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)) :
g '' image2 f s t = image2 f' s (g' '' t)

Symmetric statement to `Set.image_image2_right_comm`.

source
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)) :
image2 f (g '' s) t = g' '' image2 f' s t

Symmetric statement to `Set.image_image2_distrib_left`.

source
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)) :
image2 f s (g '' t) = g' '' image2 f' s t

Symmetric statement to `Set.image_image2_distrib_right`.

source
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)) :
image2 f s (image2 g t u) ⊆ image2 g' (image2 f₁ s t) (image2 f₂ s u)

The other direction does not hold because of the `s`-`s` cross terms on the RHS.

source
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)) :
image2 f (image2 g s t) u ⊆ image2 g' (image2 f₁ s u) (image2 f₂ t u)

The other direction does not hold because of the `u`-`u` cross terms on the RHS.

source
theorem Set.image_image2_antidistrib {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ} {s : Set α} {t : Set β} {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'} (h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)) :
g '' image2 f s t = image2 f' (g₁ '' t) (g₂ '' s)
source
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) :
g '' image2 f s t = image2 f' (g' '' t) s

Symmetric statement to `Set.image2_image_left_anticomm`.

source
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)) :
g '' image2 f s t = image2 f' t (g' '' s)

Symmetric statement to `Set.image_image2_right_anticomm`.

source
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)) :
image2 f (g '' s) t = g' '' image2 f' t s

Symmetric statement to `Set.image_image2_antidistrib_left`.

source
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)) :
image2 f s (g '' t) = g' '' image2 f' t s

Symmetric statement to `Set.image_image2_antidistrib_right`.

source
theorem Set.image2_left_identity {α : Type u_1} {β : Type u_3} {f : α → β → β} {a : α} (h : ∀ (b : β), f a b = b) (t : Set β) :
image2 f {a} t = t

If `a` is a left identity for `f : α → β → β`, then `{a}` is a left identity for `Set.image2 f`.

source
theorem Set.image2_right_identity {α : Type u_1} {β : Type u_3} {f : α → β → α} {b : β} (h : ∀ (a : α), f a b = a) (s : Set α) :
image2 f s {b} = s

If `b` is a right identity for `f : α → β → α`, then `{b}` is a right identity for `Set.image2 f`.

source
theorem Set.image2_inter_union_subset_union {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t t' : Set β} :
image2 f (s ∩ s') (t ∪ t') ⊆ image2 f s t ∪ image2 f s' t'
source
theorem Set.image2_union_inter_subset_union {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t t' : Set β} :
image2 f (s ∪ s') (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'
source
theorem Set.image2_inter_union_subset {α : Type u_1} {β : Type u_3} {f : α → α → β} {s t : Set α} (hf : ∀ (a b : α), f a b = f b a) :
image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t
source
theorem Set.image2_union_inter_subset {α : Type u_1} {β : Type u_3} {f : α → α → β} {s t : Set α} (hf : ∀ (a b : α), f a b = f b a) :
image2 f (s ∪ t) (s ∩ t) ⊆ image2 f s t