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_3} {γ : Type u_5} (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

• Set.image2 f s t = {c : γ | ∃ (a : α) (b : β), a ∈ s ∧ b ∈ t ∧ f a b = c}

@[simp]

theorem Set.mem_image2 {α : Type u_1} {β : Type u_3} {γ : Type u_5} {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_3} {γ : Type u_5} {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_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β} (hf : Function.Injective2 f) : f a b ∈ Set.image2 f s t ↔ a ∈ s ∧ b ∈ t

theorem Set.image2_subset {α : Type u_1} {β : Type u_3} {γ : Type u_5} {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_1} {β : Type u_3} {γ : Type u_5} {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_5} {f : α → β → γ} {s : Set α} {s' : Set α} {t : Set β} (hs : s ⊆ s') : Set.image2 f s t ⊆ Set.image2 f s' t

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 ⊆ Set.image2 f s t

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 ⊆ Set.image2 f s t

theorem Set.forall_image2_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {p : γ → Prop} : (∀ z ∈ Set.image2 f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)

@[simp]

theorem Set.image2_subset_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {u : Set γ} : Set.image2 f s t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u

theorem Set.image2_subset_iff_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {u : Set γ} : Set.image2 f s t ⊆ u ↔ ∀ a ∈ s, (fun (b : β) => f a b) '' t ⊆ u

theorem Set.image2_subset_iff_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {u : Set γ} : Set.image2 f s t ⊆ u ↔ ∀ b ∈ t, (fun (a : α) => f a b) '' s ⊆ u

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 = Set.image2 f s t

@[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 = Set.image2 f s t

@[simp]

theorem Set.image2_mk_eq_prod {α : Type u_1} {β : Type u_3} {s : Set α} {t : Set β} : Set.image2 Prod.mk s t = s ×ˢ t

theorem Set.image2_curry {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α × β → γ) (s : Set α) (t : Set β) : Set.image2 (fun (a : α) (b : β) => f (a, b)) s t = f '' s ×ˢ t

theorem Set.image2_swap {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α → β → γ) (s : Set α) (t : Set β) : Set.image2 f s t = Set.image2 (fun (a : β) (b : α) => f b a) t s

theorem Set.image2_union_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {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_1} {β : Type u_3} {γ : Type u_5} {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_3} {γ : Type u_5} {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_3} {γ : Type u_5} {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'

@[simp]

theorem Set.image2_empty_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {t : Set β} : Set.image2 f ∅ t = ∅

@[simp]

theorem Set.image2_empty_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} : Set.image2 f s ∅ = ∅

theorem Set.Nonempty.image2 {α : Type u_1} {β : Type u_3} {γ : Type u_5} {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_1} {β : Type u_3} {γ : Type u_5} {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_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} (h : Set.Nonempty (Set.image2 f s t)) : Set.Nonempty s

theorem Set.Nonempty.of_image2_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} (h : Set.Nonempty (Set.image2 f s t)) : Set.Nonempty t

@[simp]

theorem Set.image2_eq_empty_iff {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} : Set.image2 f s t = ∅ ↔ s = ∅ ∨ t = ∅

theorem Set.Subsingleton.image2 {α : Type u_1} {β : Type u_3} {γ : Type u_5} {s : Set α} {t : Set β} (hs : Set.Subsingleton s) (ht : Set.Subsingleton t) (f : α → β → γ) : Set.Subsingleton (Set.image2 f s t)

theorem Set.image2_inter_subset_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {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_1} {β : Type u_3} {γ : Type u_5} {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_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {t : Set β} {a : α} : Set.image2 f {a} t = f a '' t

@[simp]

theorem Set.image2_singleton_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {b : β} : Set.image2 f s {b} = (fun (a : α) => f a b) '' s

theorem Set.image2_singleton {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {a : α} {b : β} : Set.image2 f {a} {b} = {f a b}

@[simp]

theorem Set.image2_insert_left {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {a : α} : Set.image2 f (insert a s) t = (fun (b : β) => f a b) '' t ∪ Set.image2 f s t

@[simp]

theorem Set.image2_insert_right {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {b : β} : Set.image2 f s (insert b t) = (fun (a : α) => f a b) '' s ∪ Set.image2 f s t

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) : Set.image2 f s t = Set.image2 f' s t

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) : 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_3} {γ : Type u_5} {δ : Type u_7} (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

• Set.image3 g s t u = {d : δ | ∃ (a : α) (b : β) (c : γ), a ∈ s ∧ b ∈ t ∧ c ∈ u ∧ g a b c = d}

@[simp]

theorem Set.mem_image3 {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {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_3} {γ : Type u_5} {δ : Type u_7} {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_3} {γ : Type u_5} {δ : Type u_7} {g : α → β → γ → δ} {g' : α → β → γ → δ} {s : Set α} {t : Set β} {u : Set γ} (h : ∀ a ∈ s, ∀ b ∈ t, ∀ c ∈ u, g 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_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {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_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {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_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {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_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {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_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {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_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β} (f : α → γ → δ) (g : β → γ) : Set.image2 f s (g '' t) = Set.image2 (fun (a : α) (b : β) => f a (g b)) s t

@[simp]

theorem Set.image2_left {α : Type u_1} {β : Type u_3} {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_3} {s : Set α} {t : Set β} (h : Set.Nonempty s) : Set.image2 (fun (x : α) (y : β) => y) s t = t

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

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) : Set.image2 f s t = Set.image2 g t s

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)) : 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_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) : 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_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)) : 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_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 '' Set.image2 f s t = Set.image2 f' (g₁ '' s) (g₂ '' t)

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 '' 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_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 '' 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_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)) : 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_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)) : 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_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)) : 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_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)) : 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_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 '' Set.image2 f s t = Set.image2 f' (g₁ '' t) (g₂ '' s)

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 '' 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_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 '' 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_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)) : 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_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)) : 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_1} {β : Type u_3} {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_3} {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_union {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {s' : Set α} {t : Set β} {t' : Set β} : Set.image2 f (s ∩ s') (t ∪ t') ⊆ Set.image2 f s t ∪ Set.image2 f s' t'

theorem Set.image2_union_inter_subset_union {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {s' : Set α} {t : Set β} {t' : Set β} : Set.image2 f (s ∪ s') (t ∩ t') ⊆ Set.image2 f s t ∪ Set.image2 f s' t'

theorem Set.image2_inter_union_subset {α : Type u_1} {β : Type u_3} {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_3} {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