Mathlib.Data.Set.NAry

Set.mem_image2_iff theorem

(hf : Injective2 f) : f a b ∈ image2 f s t ↔ a ∈ s ∧ b ∈ t

Full source

theorem mem_image2_iff (hf : Injective2 f) : f a b ∈ image2 f s tf a b ∈ image2 f s t ↔ a ∈ s ∧ b ∈ t :=
  ⟨by
    rintro ⟨a', ha', b', hb', h⟩
    rcases hf h with ⟨rfl, rfl⟩
    exact ⟨ha', hb'⟩, fun ⟨ha, hb⟩ => mem_image2_of_mem ha hb⟩

Characterization of Membership in Binary Image via Injectivity

Informal description

For an injective binary function $f : \alpha \to \beta \to \gamma$, an element $f(a, b)$ belongs to the image $\text{image2}(f, s, t)$ if and only if $a \in s$ and $b \in t$.

Set.image2_subset theorem

(hs : s ⊆ s') (ht : t ⊆ t') : image2 f s t ⊆ image2 f s' t'

Full source

/-- image2 is monotone with respect to `⊆`. -/
@[gcongr]
theorem image2_subset (hs : s ⊆ s') (ht : t ⊆ t') : image2image2 f s t ⊆ image2 f s' t' := by
  rintro _ ⟨a, ha, b, hb, rfl⟩
  exact mem_image2_of_mem (hs ha) (ht hb)

Monotonicity of Binary Image under Subset Inclusion

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and sets $s, s' \subseteq \alpha$, $t, t' \subseteq \beta$, if $s \subseteq s'$ and $t \subseteq t'$, then the image $\text{image2}(f, s, t)$ is a subset of $\text{image2}(f, s', t')$.

Set.image2_subset_left theorem

(ht : t ⊆ t') : image2 f s t ⊆ image2 f s t'

Full source

@[gcongr]
theorem image2_subset_left (ht : t ⊆ t') : image2image2 f s t ⊆ image2 f s t' :=
  image2_subset Subset.rfl ht

Left Monotonicity of Binary Image under Right Subset Inclusion

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and sets $s \subseteq \alpha$, $t, t' \subseteq \beta$, if $t \subseteq t'$, then the image $\text{image2}(f, s, t)$ is a subset of $\text{image2}(f, s, t')$.

Set.image2_subset_right theorem

(hs : s ⊆ s') : image2 f s t ⊆ image2 f s' t

Full source

@[gcongr]
theorem image2_subset_right (hs : s ⊆ s') : image2image2 f s t ⊆ image2 f s' t :=
  image2_subset hs Subset.rfl

Right Monotonicity of Binary Image under Subset Inclusion

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and sets $s, s' \subseteq \alpha$, $t \subseteq \beta$, if $s \subseteq s'$, then the image $\{f(a, b) \mid a \in s, b \in t\}$ is a subset of $\{f(a, b) \mid a \in s', b \in t\}$.

Set.image_subset_image2_left theorem

(hb : b ∈ t) : (fun a => f a b) '' s ⊆ image2 f s t

Full source

theorem image_subset_image2_left (hb : b ∈ t) : (fun a => f a b) '' s(fun a => f a b) '' s ⊆ image2 f s t :=
  forall_mem_image.2 fun _ ha => mem_image2_of_mem ha hb

Image of Partial Application is Subset of Binary Image

Informal description

For any element $b \in t$, the image of the function $a \mapsto f(a, b)$ on the set $s$ is a subset of the binary image $\text{image2}(f, s, t)$.

Set.image_subset_image2_right theorem

(ha : a ∈ s) : f a '' t ⊆ image2 f s t

Full source

theorem image_subset_image2_right (ha : a ∈ s) : f a '' tf a '' t ⊆ image2 f s t :=
  forall_mem_image.2 fun _ => mem_image2_of_mem ha

Right Partial Image is Subset of Binary Image

Informal description

For any element $a \in s$, the image of the set $t$ under the function $f(a, \cdot)$ is a subset of the binary image $\{f(x, y) \mid x \in s, y \in t\}$.

Set.forall_mem_image2 theorem

{p : γ → Prop} : (∀ z ∈ image2 f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)

Full source

lemma forall_mem_image2 {p : γ → Prop} :
    (∀ z ∈ image2 f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y) := by aesop

Universal Property of Binary Image of Sets

Informal description

For any predicate $p$ on $\gamma$, the following are equivalent: 1. For every element $z$ in the image $\{f(x, y) \mid x \in s, y \in t\}$, the predicate $p(z)$ holds. 2. For every $x \in s$ and every $y \in t$, the predicate $p(f(x, y))$ holds.

Set.exists_mem_image2 theorem

{p : γ → Prop} : (∃ z ∈ image2 f s t, p z) ↔ ∃ x ∈ s, ∃ y ∈ t, p (f x y)

Full source

lemma exists_mem_image2 {p : γ → Prop} :
    (∃ z ∈ image2 f s t, p z) ↔ ∃ x ∈ s, ∃ y ∈ t, p (f x y) := by aesop

Existential Property of Binary Image of Sets

Informal description

For any predicate $p$ on $\gamma$, there exists an element $z$ in the image $\{f(x, y) \mid x \in s, y \in t\}$ such that $p(z)$ holds if and only if there exist $x \in s$ and $y \in t$ such that $p(f(x, y))$ holds.

Set.image2_subset_iff theorem

{u : Set γ} : image2 f s t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u

Full source

@[simp]
theorem image2_subset_iff {u : Set γ} : image2image2 f s t ⊆ uimage2 f s t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u :=
  forall_mem_image2

Subset Condition for Binary Image of Sets

Informal description

For any binary function $f \colon \alpha \to \beta \to \gamma$, sets $s \subseteq \alpha$, $t \subseteq \beta$, and $u \subseteq \gamma$, the binary image $\{f(x, y) \mid x \in s, y \in t\}$ is a subset of $u$ if and only if for every $x \in s$ and $y \in t$, the element $f(x, y)$ belongs to $u$. In other words: \[ \text{image2}(f, s, t) \subseteq u \leftrightarrow \forall x \in s, \forall y \in t, f(x, y) \in u. \]

Set.image2_subset_iff_left theorem

: image2 f s t ⊆ u ↔ ∀ a ∈ s, (fun b => f a b) '' t ⊆ u

Full source

theorem image2_subset_iff_left : image2image2 f s t ⊆ uimage2 f s t ⊆ u ↔ ∀ a ∈ s, (fun b => f a b) '' t ⊆ u := by
  simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage]

Left Argument Subset Condition for Binary Image

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, $u \subseteq \gamma$, the binary image $\{f(a, b) \mid a \in s, b \in t\}$ is a subset of $u$ if and only if for every $a \in s$, the image $\{f(a, b) \mid b \in t\}$ is a subset of $u$.

Set.image2_subset_iff_right theorem

: image2 f s t ⊆ u ↔ ∀ b ∈ t, (fun a => f a b) '' s ⊆ u

Full source

theorem image2_subset_iff_right : image2image2 f s t ⊆ uimage2 f s t ⊆ u ↔ ∀ b ∈ t, (fun a => f a b) '' s ⊆ u := by
  simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage, @forall₂_swap α]

Right Partial Application Characterizes Binary Image Subset

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$, sets $s \subseteq \alpha$, $t \subseteq \beta$, and $u \subseteq \gamma$, the binary image $\text{image2}(f, s, t)$ is a subset of $u$ if and only if for every $b \in t$, the image of $s$ under the partially applied function $f(\cdot, b)$ is a subset of $u$. In other words: \[ \{f(a, b) \mid a \in s, b \in t\} \subseteq u \leftrightarrow \forall b \in t, \{f(a, b) \mid a \in s\} \subseteq u. \]

Set.image_prod theorem

: (fun x : α × β ↦ f x.1 x.2) '' s ×ˢ t = image2 f s t

Full source

@[simp]
lemma image_prod : (fun x : α × β ↦ f x.1 x.2) '' s ×ˢ t = image2 f s t :=
  ext fun _ ↦ by simp [and_assoc]

Equality of Uncurried Image and Binary Image on Cartesian Product

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, the image of the Cartesian product $s \times t$ under the uncurried function $(x,y) \mapsto f(x,y)$ is equal to the binary image $\text{image2}(f, s, t)$. In other words, $$ \{(f(x,y) \mid (x,y) \in s \times t\} = \{f(x,y) \mid x \in s, y \in t\}. $$

Set.image_uncurry_prod theorem

(s : Set α) (t : Set β) : uncurry f '' s ×ˢ t = image2 f s t

Full source

@[simp] lemma image_uncurry_prod (s : Set α) (t : Set β) : uncurryuncurry f '' s ×ˢ t = image2 f s t :=
  image_prod _

Equality of Uncurried Image and Binary Image on Cartesian Product

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the Cartesian product $s \times t$ under the uncurried function $f : \alpha \times \beta \to \gamma$ equals the binary image $\text{image2}(f, s, t)$. That is, $$ \{f(x,y) \mid (x,y) \in s \times t\} = \{f(x,y) \mid x \in s, y \in t\}. $$

Set.image2_mk_eq_prod theorem

: image2 Prod.mk s t = s ×ˢ t

Full source

@[simp] lemma image2_mk_eq_prod : image2 Prod.mk s t = s ×ˢ t := ext <| by simp

Image of Pairing Function Equals Cartesian Product

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the pairing function $\text{Prod.mk}$ on $s \times t$ equals the Cartesian product $s \times t$. That is, \[ \{(a, b) \mid a \in s, b \in t\} = s \times t. \]

Set.image2_curry theorem

(f : α × β → γ) (s : Set α) (t : Set β) : image2 (fun a b ↦ f (a, b)) s t = f '' s ×ˢ t

Full source

@[simp]
lemma image2_curry (f : α × β → γ) (s : Set α) (t : Set β) :
    image2 (fun a b ↦ f (a, b)) s t = f '' s ×ˢ t := by
  simp [← image_uncurry_prod, uncurry]

Image of Curried Function Equals Image on Cartesian Product

Informal description

For any function $f : \alpha \times \beta \to \gamma$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, the image of the curried function $\lambda a b, f(a, b)$ on $s \times t$ is equal to the image of $f$ on the Cartesian product $s \times t$. That is, \[ \{f(a, b) \mid a \in s, b \in t\} = f(s \times t). \]

Set.image2_swap theorem

(s : Set α) (t : Set β) : image2 f s t = image2 (fun a b => f b a) t s

Full source

theorem image2_swap (s : Set α) (t : Set β) : image2 f s t = image2 (fun a b => f b a) t s := by
  ext
  constructor <;> rintro ⟨a, ha, b, hb, rfl⟩ <;> exact ⟨b, hb, a, ha, rfl⟩

Commutativity of Binary Image: $\text{image2}(f, s, t) = \text{image2}(f \circ \text{swap}, t, s)$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, the image of $f$ on $s \times t$ is equal to the image of the swapped function $\lambda a b, f b a$ on $t \times s$. That is, \[ \{f(a, b) \mid a \in s, b \in t\} = \{f(b, a) \mid a \in s, b \in t\}. \]

Set.image2_union_left theorem

: image2 f (s ∪ s') t = image2 f s t ∪ image2 f s' t

Full source

theorem image2_union_left : image2 f (s ∪ s') t = image2image2 f s t ∪ image2 f s' t := by
  simp_rw [← image_prod, union_prod, image_union]

Distributivity of Binary Image over Union in First Argument: $\text{image2}(f, s \cup s', t) = \text{image2}(f, s, t) \cup \text{image2}(f, s', t)$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and sets $s, s' \subseteq \alpha$, $t \subseteq \beta$, the image of $f$ on the union $(s \cup s') \times t$ is equal to the union of the images of $f$ on $s \times t$ and $s' \times t$. That is, \[ \{f(a, b) \mid a \in s \cup s', b \in t\} = \{f(a, b) \mid a \in s, b \in t\} \cup \{f(a, b) \mid a \in s', b \in t\}. \]

Set.image2_union_right theorem

: image2 f s (t ∪ t') = image2 f s t ∪ image2 f s t'

Full source

theorem image2_union_right : image2 f s (t ∪ t') = image2image2 f s t ∪ image2 f s t' := by
  rw [← image2_swap, image2_union_left, image2_swap f, image2_swap f]

Distributivity of Binary Image over Union in Second Argument: $\text{image2}(f, s, t \cup t') = \text{image2}(f, s, t) \cup \text{image2}(f, s, t')$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and sets $s \subseteq \alpha$, $t, t' \subseteq \beta$, the image of $f$ on $s \times (t \cup t')$ is equal to the union of the images of $f$ on $s \times t$ and $s \times t'$. That is, \[ \{f(a, b) \mid a \in s, b \in t \cup t'\} = \{f(a, b) \mid a \in s, b \in t\} \cup \{f(a, b) \mid a \in s, b \in t'\}. \]

Set.image2_inter_left theorem

(hf : Injective2 f) : image2 f (s ∩ s') t = image2 f s t ∩ image2 f s' t

Full source

lemma image2_inter_left (hf : Injective2 f) :
    image2 f (s ∩ s') t = image2image2 f s t ∩ image2 f s' t := by
  simp_rw [← image_uncurry_prod, inter_prod, image_inter hf.uncurry]

Intersection Preservation in First Argument for Binary Image under Injective Functions: $\text{image2}(f, s \cap s', t) = \text{image2}(f, s, t) \cap \text{image2}(f, s', t)$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ that is injective in both arguments, and any sets $s, s' \subseteq \alpha$, $t \subseteq \beta$, the image of $f$ on the intersection $(s \cap s') \times t$ is equal to the intersection of the images of $f$ on $s \times t$ and $s' \times t$. That is, \[ \{f(a, b) \mid a \in s \cap s', b \in t\} = \{f(a, b) \mid a \in s, b \in t\} \cap \{f(a, b) \mid a \in s', b \in t\}. \]

Set.image2_inter_right theorem

(hf : Injective2 f) : image2 f s (t ∩ t') = image2 f s t ∩ image2 f s t'

Full source

lemma image2_inter_right (hf : Injective2 f) :
    image2 f s (t ∩ t') = image2image2 f s t ∩ image2 f s t' := by
  simp_rw [← image_uncurry_prod, prod_inter, image_inter hf.uncurry]

Distributivity of Binary Image over Intersection in Second Argument for Injective Functions

Informal description

For any injective binary function $f : \alpha \to \beta \to \gamma$ and sets $s \subseteq \alpha$, $t, t' \subseteq \beta$, the image of $f$ on $s \times (t \cap t')$ is equal to the intersection of the images of $f$ on $s \times t$ and $s \times t'$. That is, \[ \{f(a, b) \mid a \in s, b \in t \cap t'\} = \{f(a, b) \mid a \in s, b \in t\} \cap \{f(a, b) \mid a \in s, b \in t'\}. \]

Set.image2_empty_left theorem

: image2 f ∅ t = ∅

Full source

@[simp]
theorem image2_empty_left : image2 f ∅ t = ∅ :=
  ext <| by simp

Empty Set Left Image Property: $\text{image2}(f, \emptyset, t) = \emptyset$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and any set $t \subseteq \beta$, the image of $f$ applied to the empty set and $t$ is the empty set, i.e., $\text{image2}(f, \emptyset, t) = \emptyset$.

Set.image2_empty_right theorem

: image2 f s ∅ = ∅

Full source

@[simp]
theorem image2_empty_right : image2 f s ∅ = ∅ :=
  ext <| by simp

Empty Set Right Image Property: $\text{image2}(f, s, \emptyset) = \emptyset$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and any set $s \subseteq \alpha$, the image of $f$ applied to $s$ and the empty set is the empty set, i.e., $\text{image2}(f, s, \emptyset) = \emptyset$.

Set.Nonempty.image2 theorem

: s.Nonempty → t.Nonempty → (image2 f s t).Nonempty

Full source

theorem Nonempty.image2 : s.Nonempty → t.Nonempty → (image2 f s t).Nonempty :=
  fun ⟨_, ha⟩ ⟨_, hb⟩ => ⟨_, mem_image2_of_mem ha hb⟩

Nonempty Image of Nonempty Sets under Binary Function

Informal description

For any nonempty sets $s \subseteq \alpha$ and $t \subseteq \beta$, and any binary function $f : \alpha \to \beta \to \gamma$, the image $\text{image2}(f, s, t)$ is nonempty.

Set.image2_nonempty_iff theorem

: (image2 f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Full source

@[simp]
theorem image2_nonempty_iff : (image2 f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty :=
  ⟨fun ⟨_, a, ha, b, hb, _⟩ => ⟨⟨a, ha⟩, b, hb⟩, fun h => h.1.image2 h.2⟩

Nonempty Image of Binary Function on Sets iff Both Sets Nonempty

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, the image $\text{image2}(f, s, t)$ is nonempty if and only if both $s$ and $t$ are nonempty.

Set.Nonempty.of_image2_left theorem

(h : (Set.image2 f s t).Nonempty) : s.Nonempty

Full source

theorem Nonempty.of_image2_left (h : (Set.image2 f s t).Nonempty) : s.Nonempty :=
  (image2_nonempty_iff.1 h).1

Nonempty Image Implies Nonempty Left Set

Informal description

If the image $\text{image2}(f, s, t)$ of a binary function $f : \alpha \to \beta \to \gamma$ on sets $s \subseteq \alpha$ and $t \subseteq \beta$ is nonempty, then the set $s$ is nonempty.

Set.Nonempty.of_image2_right theorem

(h : (Set.image2 f s t).Nonempty) : t.Nonempty

Full source

theorem Nonempty.of_image2_right (h : (Set.image2 f s t).Nonempty) : t.Nonempty :=
  (image2_nonempty_iff.1 h).2

Nonemptiness of Second Set in Binary Image Implies Nonemptiness of Second Set

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, if the image $\text{image2}(f, s, t)$ is nonempty, then the set $t$ is nonempty.

Set.image2_eq_empty_iff theorem

: image2 f s t = ∅ ↔ s = ∅ ∨ t = ∅

Full source

@[simp]
theorem image2_eq_empty_iff : image2image2 f s t = ∅ ↔ s = ∅ ∨ t = ∅ := by
  rw [← not_nonempty_iff_eq_empty, image2_nonempty_iff, not_and_or]
  simp [not_nonempty_iff_eq_empty]

Empty Image of Binary Function on Sets iff Either Set Empty

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, the image $\text{image2}(f, s, t)$ is empty if and only if either $s$ is empty or $t$ is empty. That is, $\text{image2}(f, s, t) = \emptyset \leftrightarrow s = \emptyset \lor t = \emptyset$.

Set.Subsingleton.image2 theorem

(hs : s.Subsingleton) (ht : t.Subsingleton) (f : α → β → γ) : (image2 f s t).Subsingleton

Full source

theorem Subsingleton.image2 (hs : s.Subsingleton) (ht : t.Subsingleton) (f : α → β → γ) :
    (image2 f s t).Subsingleton := by
  rw [← image_prod]
  apply (hs.prod ht).image

Subsingleton Property of Binary Image on Subsingleton Sets

Informal description

If $s \subseteq \alpha$ and $t \subseteq \beta$ are subsingleton sets (i.e., each contains at most one element), then for any binary function $f : \alpha \to \beta \to \gamma$, the image $\text{image2}(f, s, t)$ is also a subsingleton set in $\gamma$.

Set.image2_inter_subset_left theorem

: image2 f (s ∩ s') t ⊆ image2 f s t ∩ image2 f s' t

Full source

theorem image2_inter_subset_left : image2image2 f (s ∩ s') t ⊆ image2 f s t ∩ image2 f s' t :=
  Monotone.map_inf_le (fun _ _ ↦ image2_subset_right) s s'

Left Intersection Subset Property for Binary Image: $\text{image2}(f, s \cap s', t) \subseteq \text{image2}(f, s, t) \cap \text{image2}(f, s', t)$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and sets $s, s' \subseteq \alpha$, $t \subseteq \beta$, the image $\{f(a, b) \mid a \in s \cap s', b \in t\}$ is a subset of $\{f(a, b) \mid a \in s, b \in t\} \cap \{f(a, b) \mid a \in s', b \in t\}$.

Set.image2_inter_subset_right theorem

: image2 f s (t ∩ t') ⊆ image2 f s t ∩ image2 f s t'

Full source

theorem image2_inter_subset_right : image2image2 f s (t ∩ t') ⊆ image2 f s t ∩ image2 f s t' :=
  Monotone.map_inf_le (fun _ _ ↦ image2_subset_left) t t'

Right Intersection Subset Property of Binary Image

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and sets $s \subseteq \alpha$, $t, t' \subseteq \beta$, the image $\text{image2}(f, s, t \cap t')$ is a subset of the intersection $\text{image2}(f, s, t) \cap \text{image2}(f, s, t')$.

Set.image2_singleton_left theorem

: image2 f { a } t = f a '' t

Full source

@[simp]
theorem image2_singleton_left : image2 f {a} t = f a '' t :=
  ext fun x => by simp

Image of Binary Function with Singleton Left Argument: $\text{image2}(f, \{a\}, t) = \{f(a, b) \mid b \in t\}$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$, any singleton set $\{a\} \subseteq \alpha$, and any set $t \subseteq \beta$, the image $\text{image2}(f, \{a\}, t)$ is equal to the image of $t$ under the unary function $f(a)$. In other words, $\text{image2}(f, \{a\}, t) = \{f(a, b) \mid b \in t\}$.

Set.image2_singleton_right theorem

: image2 f s { b } = (fun a => f a b) '' s

Full source

@[simp]
theorem image2_singleton_right : image2 f s {b} = (fun a => f a b) '' s :=
  ext fun x => by simp

Image of Binary Function with Singleton Right Argument: $\text{image2}(f, s, \{b\}) = \{f(a, b) \mid a \in s\}$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$, any set $s \subseteq \alpha$, and any singleton set $\{b\} \subseteq \beta$, the image $\text{image2}(f, s, \{b\})$ is equal to the image of $s$ under the unary function $\lambda a, f(a, b)$. In other words, $\text{image2}(f, s, \{b\}) = \{f(a, b) \mid a \in s\}$.

Set.image2_singleton theorem

: image2 f { a } { b } = {f a b}

Full source

theorem image2_singleton : image2 f {a} {b} = {f a b} := by simp

Image of Binary Function on Singleton Sets: $\text{image2}(f, \{a\}, \{b\}) = \{f(a, b)\}$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and any elements $a \in \alpha$, $b \in \beta$, the image of the singleton sets $\{a\}$ and $\{b\}$ under $f$ is the singleton set $\{f(a, b)\}$. In other words, $\text{image2}(f, \{a\}, \{b\}) = \{f(a, b)\}$.

Set.image2_insert_left theorem

: image2 f (insert a s) t = (fun b => f a b) '' t ∪ image2 f s t

Full source

@[simp]
theorem image2_insert_left : image2 f (insert a s) t = (fun b => f a b) '' t(fun b => f a b) '' t ∪ image2 f s t := by
  rw [insert_eq, image2_union_left, image2_singleton_left]

Binary Image with Insertion in First Argument: $\text{image2}(f, \{a\} \cup s, t) = \{f(a, b) \mid b \in t\} \cup \text{image2}(f, s, t)$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$, any element $a \in \alpha$, any set $s \subseteq \alpha$, and any set $t \subseteq \beta$, the image of $f$ on the set $\text{insert}(a, s) \times t$ is equal to the union of the image of $t$ under the function $\lambda b, f(a, b)$ and the image of $f$ on $s \times t$. In other words, \[ \{f(x, b) \mid x \in \{a\} \cup s, b \in t\} = \{f(a, b) \mid b \in t\} \cup \{f(x, b) \mid x \in s, b \in t\}. \]

Set.image2_insert_right theorem

: image2 f s (insert b t) = (fun a => f a b) '' s ∪ image2 f s t

Full source

@[simp]
theorem image2_insert_right : image2 f s (insert b t) = (fun a => f a b) '' s(fun a => f a b) '' s ∪ image2 f s t := by
  rw [insert_eq, image2_union_right, image2_singleton_right]

Binary Image with Insertion in Second Argument: $\text{image2}(f, s, \{b\} \cup t) = \{f(a, b) \mid a \in s\} \cup \text{image2}(f, s, t)$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$, any set $s \subseteq \alpha$, any element $b \in \beta$, and any set $t \subseteq \beta$, the image of $f$ on $s \times \text{insert}(b, t)$ is equal to the union of the image of $s$ under the function $\lambda a, f(a, b)$ and the image of $f$ on $s \times t$. That is, \[ \{f(a, y) \mid a \in s, y \in \{b\} \cup t\} = \{f(a, b) \mid a \in s\} \cup \{f(a, y) \mid a \in s, y \in t\}. \]

Set.image2_congr theorem

(h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b) : image2 f s t = image2 f' s t

Full source

@[congr]
theorem image2_congr (h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b) : image2 f s t = image2 f' s t := by
  ext
  constructor <;> rintro ⟨a, ha, b, hb, rfl⟩ <;> exact ⟨a, ha, b, hb, by rw [h a ha b hb]⟩

Congruence of Binary Image under Pointwise Equality

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, and functions $f, f' : \alpha \to \beta \to \gamma$, if $f(a, b) = f'(a, b)$ for all $a \in s$ and $b \in t$, then the binary images $\text{image2}(f, s, t)$ and $\text{image2}(f', s, t)$ are equal.

Set.image2_congr' theorem

(h : ∀ a b, f a b = f' a b) : image2 f s t = image2 f' s t

Full source

/-- A common special case of `image2_congr` -/
theorem image2_congr' (h : ∀ a b, f a b = f' a b) : image2 f s t = image2 f' s t :=
  image2_congr fun a _ b _ => h a b

Binary Image Congruence under Global Pointwise Equality

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, and functions $f, f' : \alpha \to \beta \to \gamma$, if $f(a, b) = f'(a, b)$ for all $a \in \alpha$ and $b \in \beta$, then the binary images $\text{image2}(f, s, t)$ and $\text{image2}(f', s, t)$ are equal.

Set.image_image2 theorem

(f : α → β → γ) (g : γ → δ) : g '' image2 f s t = image2 (fun a b => g (f a b)) s t

Full source

theorem image_image2 (f : α → β → γ) (g : γ → δ) :
    g '' image2 f s t = image2 (fun a b => g (f a b)) s t := by
  simp only [← image_prod, image_image]

Image of Binary Image Equals Binary Image of Composition: $g(f(s, t)) = (g \circ f)(s, t)$

Informal description

For any functions $f \colon \alpha \to \beta \to \gamma$ and $g \colon \gamma \to \delta$, and any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the binary image $\text{image2}(f, s, t)$ under $g$ is equal to the binary image of $s$ and $t$ under the composition $\lambda a b, g(f(a, b))$. In symbols: \[ g(\text{image2}(f, s, t)) = \text{image2}(\lambda a b, g(f(a, b)), s, t). \]

Set.image2_image_left theorem

(f : γ → β → δ) (g : α → γ) : image2 f (g '' s) t = image2 (fun a b => f (g a) b) s t

Full source

theorem image2_image_left (f : γ → β → δ) (g : α → γ) :
    image2 f (g '' s) t = image2 (fun a b => f (g a) b) s t := by
  ext; simp

Left Composition Property of Binary Image: $\text{image2}(f, g(s), t) = \text{image2}(f \circ g, s, t)$

Informal description

For any function $f : \gamma \to \beta \to \delta$, a function $g : \alpha \to \gamma$, and sets $s \subseteq \alpha$, $t \subseteq \beta$, the image of $f$ over the image of $g$ applied to $s$ and $t$ satisfies: \[ \text{image2}(f, g(s), t) = \text{image2}(\lambda a b, f(g(a), b), s, t) \] where $\text{image2}(f, s, t)$ denotes the set $\{f(a, b) \mid a \in s, b \in t\}$.

Set.image2_image_right theorem

(f : α → γ → δ) (g : β → γ) : image2 f s (g '' t) = image2 (fun a b => f a (g b)) s t

Full source

theorem image2_image_right (f : α → γ → δ) (g : β → γ) :
    image2 f s (g '' t) = image2 (fun a b => f a (g b)) s t := by
  ext; simp

Image of Binary Function with Right Composition

Informal description

For any function $f : \alpha \to \gamma \to \delta$, a function $g : \beta \to \gamma$, and sets $s \subseteq \alpha$, $t \subseteq \beta$, the image of $f$ over $s$ and the image of $g$ over $t$ satisfies: \[ \text{image2}(f, s, g(t)) = \text{image2}(\lambda a b, f(a, g(b)), s, t) \] where $\text{image2}(f, s, t)$ denotes the set $\{f(a, b) \mid a \in s, b \in t\}$.

Set.image2_left theorem

(h : t.Nonempty) : image2 (fun x _ => x) s t = s

Full source

@[simp]
theorem image2_left (h : t.Nonempty) : image2 (fun x _ => x) s t = s := by
  simp [nonempty_def.mp h, Set.ext_iff]

Left Projection Image of Nonempty Set

Informal description

For any nonempty set $t$ and any set $s$, the binary image of the projection function $\lambda x \_, x$ over $s$ and $t$ equals $s$, i.e., \[ \text{image2}(\lambda x \_, x, s, t) = s. \]

Set.image2_right theorem

(h : s.Nonempty) : image2 (fun _ y => y) s t = t

Full source

@[simp]
theorem image2_right (h : s.Nonempty) : image2 (fun _ y => y) s t = t := by
  simp [nonempty_def.mp h, Set.ext_iff]

Right Projection Image of Nonempty Set

Informal description

For any nonempty set $s$ over a type $\alpha$ and any set $t$ over a type $\beta$, the image of the projection function $\lambda \_ y \mapsto y$ over $s$ and $t$ equals $t$, i.e., \[ \text{image2}(\lambda \_ y \mapsto y, s, t) = t. \]

Set.image2_range theorem

 (f : α' → β' → γ) (g : α → α') (h : β → β') : image2 f (range g) (range h) = range fun x : α × β ↦ f (g x.1) (h x.2)

Full source

lemma image2_range (f : α' → β' → γ) (g : α → α') (h : β → β') :
    image2 f (range g) (range h) = range fun x : α × β ↦ f (g x.1) (h x.2) := by
  simp_rw [← image_univ, image2_image_left, image2_image_right, ← image_prod, univ_prod_univ]

Range of Binary Image Equals Range of Composed Function: $\text{image2}(f, \text{range}(g), \text{range}(h)) = \text{range}((x,y) \mapsto f(g(x), h(y)))$

Informal description

For any binary function $f : \alpha' \to \beta' \to \gamma$ and functions $g : \alpha \to \alpha'$, $h : \beta \to \beta'$, the image of $f$ over the ranges of $g$ and $h$ equals the range of the function $\lambda (x,y) \in \alpha \times \beta, f(g(x), h(y))$. That is, \[ \text{image2}(f, \text{range}(g), \text{range}(h)) = \text{range}(\lambda (x,y), f(g(x), h(y))). \]

Set.image2_assoc theorem

 {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)

Full source

theorem image2_assoc {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) :=
  eq_of_forall_subset_iff fun _ ↦ by simp only [image2_subset_iff, forall_mem_image2, h_assoc]

Associativity of Binary Image Operation

Informal description

Let $f : \delta \to \gamma \to \varepsilon$, $g : \alpha \to \beta \to \delta$, $f' : \alpha \to \varepsilon' \to \varepsilon$, and $g' : \beta \to \gamma \to \varepsilon'$ be functions such that for all $a \in \alpha$, $b \in \beta$, and $c \in \gamma$, the associativity condition $f(g(a,b),c) = f'(a, g'(b,c))$ holds. Then for any sets $s \subseteq \alpha$, $t \subseteq \beta$, and $u \subseteq \gamma$, we have: \[ \text{image2}(f, \text{image2}(g, s, t), u) = \text{image2}(f', s, \text{image2}(g', t, u)). \]

Set.image2_comm theorem

{g : β → α → γ} (h_comm : ∀ a b, f a b = g b a) : image2 f s t = image2 g t s

Full source

theorem image2_comm {g : β → α → γ} (h_comm : ∀ a b, f a b = g b a) : image2 f s t = image2 g t s :=
  (image2_swap _ _ _).trans <| by simp_rw [h_comm]

Commutativity of Binary Image: $\text{image2}(f, s, t) = \text{image2}(g, t, s)$ when $f(a,b)=g(b,a)$

Informal description

For any binary functions $f : \alpha \to \beta \to \gamma$ and $g : \beta \to \alpha \to \gamma$ such that $f(a, b) = g(b, a)$ for all $a \in \alpha$ and $b \in \beta$, and for any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the binary images satisfy $\text{image2}(f, s, t) = \text{image2}(g, t, s)$.

Set.image2_left_comm theorem

 {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)

Full source

theorem image2_left_comm {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) := by
  rw [image2_swap f', image2_swap f]
  exact image2_assoc fun _ _ _ => h_left_comm _ _ _

Left-commutativity of binary image operation

Informal description

Let $f : \alpha \to \delta \to \varepsilon$, $g : \beta \to \gamma \to \delta$, $f' : \alpha \to \gamma \to \delta'$, and $g' : \beta \to \delta' \to \varepsilon$ be functions such that for all $a \in \alpha$, $b \in \beta$, and $c \in \gamma$, the left-commutativity condition $f(a, g(b, c)) = g'(b, f'(a, c))$ holds. Then for any sets $s \subseteq \alpha$, $t \subseteq \beta$, and $u \subseteq \gamma$, we have: \[ \text{image2}(f, s, \text{image2}(g, t, u)) = \text{image2}(g', t, \text{image2}(f', s, u)). \]

Set.image2_right_comm theorem

 {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

Full source

theorem image2_right_comm {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 := by
  rw [image2_swap g, image2_swap g']
  exact image2_assoc fun _ _ _ => h_right_comm _ _ _

Right Commutativity of Binary Image Operation

Informal description

Let $f : \delta \to \gamma \to \varepsilon$, $g : \alpha \to \beta \to \delta$, $f' : \alpha \to \gamma \to \delta'$, and $g' : \delta' \to \beta \to \varepsilon$ be functions such that for all $a \in \alpha$, $b \in \beta$, and $c \in \gamma$, the right-commutativity condition $f(g(a,b), c) = g'(f'(a,c), b)$ holds. Then for any sets $s \subseteq \alpha$, $t \subseteq \beta$, and $u \subseteq \gamma$, we have: \[ \text{image2}(f, \text{image2}(g, s, t), u) = \text{image2}(g', \text{image2}(f', s, u), t). \]

Set.image2_image2_image2_comm theorem

 {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)

Full source

theorem image2_image2_image2_comm {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) := by
  ext; constructor
  · rintro ⟨_, ⟨a, ha, b, hb, rfl⟩, _, ⟨c, hc, d, hd, rfl⟩, rfl⟩
    exact ⟨_, ⟨a, ha, c, hc, rfl⟩, _, ⟨b, hb, d, hd, rfl⟩, (h_comm _ _ _ _).symm⟩
  · rintro ⟨_, ⟨a, ha, c, hc, rfl⟩, _, ⟨b, hb, d, hd, rfl⟩, rfl⟩
    exact ⟨_, ⟨a, ha, b, hb, rfl⟩, _, ⟨c, hc, d, hd, rfl⟩, h_comm _ _ _ _⟩

Commutativity of Nested Binary Images of Sets

Informal description

Let $f : \varepsilon \to \zeta \to \nu$, $g : \alpha \to \beta \to \varepsilon$, $h : \gamma \to \delta \to \zeta$, $f' : \varepsilon' \to \zeta' \to \nu$, $g' : \alpha \to \gamma \to \varepsilon'$, and $h' : \beta \to \delta \to \zeta'$ be functions. Suppose that for all $a \in \alpha$, $b \in \beta$, $c \in \gamma$, $d \in \delta$, the following commutation relation holds: $$f(g(a,b), h(c,d)) = f'(g'(a,c), h'(b,d)).$$ Then for any sets $s \subseteq \alpha$, $t \subseteq \beta$, $u \subseteq \gamma$, $v \subseteq \delta$, we have: $$\text{image2}\ f\ (\text{image2}\ g\ s\ t)\ (\text{image2}\ h\ u\ v) = \text{image2}\ f'\ (\text{image2}\ g'\ s\ u)\ (\text{image2}\ h'\ t\ v).$$

Set.image_image2_distrib theorem

 {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'} (h_distrib : ∀ a b, g (f a b) = f' (g₁ a) (g₂ b)) :
  (image2 f s t).image g = image2 f' (s.image g₁) (t.image g₂)

Full source

theorem image_image2_distrib {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'}
    (h_distrib : ∀ a b, g (f a b) = f' (g₁ a) (g₂ b)) :
    (image2 f s t).image g = image2 f' (s.image g₁) (t.image g₂) := by
  simp_rw [image_image2, image2_image_left, image2_image_right, h_distrib]

Distributivity of Image over Binary Image: $g(f(s, t)) = f'(g_1(s), g_2(t))$

Informal description

Let $f \colon \alpha \to \beta \to \gamma$ be a binary function, $g \colon \gamma \to \delta$ a function, and $f' \colon \alpha' \to \beta' \to \delta$ another binary function. Suppose there exist functions $g_1 \colon \alpha \to \alpha'$ and $g_2 \colon \beta \to \beta'$ such that for all $a \in \alpha$ and $b \in \beta$, the distributive property $g(f(a, b)) = f'(g_1(a), g_2(b))$ holds. Then for any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the binary image $\text{image2}(f, s, t)$ under $g$ equals the binary image of $g_1(s)$ and $g_2(t)$ under $f'$: \[ g(\text{image2}(f, s, t)) = \text{image2}(f', g_1(s), g_2(t)). \]

Set.image_image2_distrib_left theorem

 {g : γ → δ} {f' : α' → β → δ} {g' : α → α'} (h_distrib : ∀ a b, g (f a b) = f' (g' a) b) :
  (image2 f s t).image g = image2 f' (s.image g') t

Full source

/-- Symmetric statement to `Set.image2_image_left_comm`. -/
theorem image_image2_distrib_left {g : γ → δ} {f' : α' → β → δ} {g' : α → α'}
    (h_distrib : ∀ a b, g (f a b) = f' (g' a) b) :
    (image2 f s t).image g = image2 f' (s.image g') t :=
  (image_image2_distrib h_distrib).trans <| by rw [image_id']

Left Distributivity of Image over Binary Image: $g(f(s, t)) = f'(g'(s), t)$

Informal description

Let $f \colon \alpha \to \beta \to \gamma$ be a binary function, $g \colon \gamma \to \delta$ a function, and $f' \colon \alpha' \to \beta \to \delta$ another binary function. Suppose there exists a function $g' \colon \alpha \to \alpha'$ such that for all $a \in \alpha$ and $b \in \beta$, the distributive property $g(f(a, b)) = f'(g'(a), b)$ holds. Then for any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the binary image $\text{image2}(f, s, t)$ under $g$ equals the binary image of $g'(s)$ and $t$ under $f'$: \[ g(\text{image2}(f, s, t)) = \text{image2}(f', g'(s), t). \]

Set.image_image2_distrib_right theorem

 {g : γ → δ} {f' : α → β' → δ} {g' : β → β'} (h_distrib : ∀ a b, g (f a b) = f' a (g' b)) :
  (image2 f s t).image g = image2 f' s (t.image g')

Full source

/-- Symmetric statement to `Set.image_image2_right_comm`. -/
theorem image_image2_distrib_right {g : γ → δ} {f' : α → β' → δ} {g' : β → β'}
    (h_distrib : ∀ a b, g (f a b) = f' a (g' b)) :
    (image2 f s t).image g = image2 f' s (t.image g') :=
  (image_image2_distrib h_distrib).trans <| by rw [image_id']

Right Distributivity of Image over Binary Image: $g(f(s, t)) = f'(s, g'(t))$

Informal description

Let $f \colon \alpha \to \beta \to \gamma$ be a binary function, $g \colon \gamma \to \delta$ a function, and $f' \colon \alpha \to \beta' \to \delta$ another binary function. Suppose there exists a function $g' \colon \beta \to \beta'$ such that for all $a \in \alpha$ and $b \in \beta$, the distributive property $g(f(a, b)) = f'(a, g'(b))$ holds. Then for any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the binary image $\text{image2}(f, s, t)$ under $g$ equals the binary image of $s$ and $g'(t)$ under $f'$: \[ g(\text{image2}(f, s, t)) = \text{image2}(f', s, g'(t)). \]

Set.image2_image_left_comm theorem

 {f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ} (h_left_comm : ∀ a b, f (g a) b = g' (f' a b)) :
  image2 f (s.image g) t = (image2 f' s t).image g'

Full source

/-- Symmetric statement to `Set.image_image2_distrib_left`. -/
theorem image2_image_left_comm {f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ}
    (h_left_comm : ∀ a b, f (g a) b = g' (f' a b)) :
    image2 f (s.image g) t = (image2 f' s t).image g' :=
  (image_image2_distrib_left fun a b => (h_left_comm a b).symm).symm

Left Commutativity of Binary Image under Function Composition: $f(g(s), t) = g'(f'(s, t))$

Informal description

Let $f \colon \alpha' \to \beta \to \gamma$, $g \colon \alpha \to \alpha'$, $f' \colon \alpha \to \beta \to \delta$, and $g' \colon \delta \to \gamma$ be functions such that for all $a \in \alpha$ and $b \in \beta$, the left-commutative property $f(g(a), b) = g'(f'(a, b))$ holds. Then for any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the binary image of $g(s)$ and $t$ under $f$ equals the image of the binary image of $s$ and $t$ under $f'$ composed with $g'$: \[ \text{image2}(f, g(s), t) = g'(\text{image2}(f', s, t)). \]

Set.image_image2_right_comm theorem

 {f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ} (h_right_comm : ∀ a b, f a (g b) = g' (f' a b)) :
  image2 f s (t.image g) = (image2 f' s t).image g'

Full source

/-- Symmetric statement to `Set.image_image2_distrib_right`. -/
theorem image_image2_right_comm {f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ}
    (h_right_comm : ∀ a b, f a (g b) = g' (f' a b)) :
    image2 f s (t.image g) = (image2 f' s t).image g' :=
  (image_image2_distrib_right fun a b => (h_right_comm a b).symm).symm

Right Commutativity of Image and Binary Image: $f(s, g(t)) = g'(f'(s, t))$

Informal description

Let $f \colon \alpha \to \beta' \to \gamma$, $g \colon \beta \to \beta'$, $f' \colon \alpha \to \beta \to \delta$, and $g' \colon \delta \to \gamma$ be functions such that for all $a \in \alpha$ and $b \in \beta$, the right-commutativity condition $f(a, g(b)) = g'(f'(a, b))$ holds. Then for any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the binary image of $s$ and $g(t)$ under $f$ equals the image under $g'$ of the binary image of $s$ and $t$ under $f'$: \[ \text{image2}(f, s, g(t)) = g'(\text{image2}(f', s, t)). \]

Set.image2_distrib_subset_left theorem

 {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)

Full source

/-- The other direction does not hold because of the `s`-`s` cross terms on the RHS. -/
theorem image2_distrib_subset_left {f : α → δ → ε} {g : β → γ → δ} {f₁ : α → β → β'}
    {f₂ : α → γ → γ'} {g' : β' → γ' → ε} (h_distrib : ∀ a b c, f a (g b c) = g' (f₁ a b) (f₂ a c)) :
    image2image2 f s (image2 g t u) ⊆ image2 g' (image2 f₁ s t) (image2 f₂ s u) := by
  rintro _ ⟨a, ha, _, ⟨b, hb, c, hc, rfl⟩, rfl⟩
  rw [h_distrib]
  exact mem_image2_of_mem (mem_image2_of_mem ha hb) (mem_image2_of_mem ha hc)

Left Distributivity of Binary Image under Function Composition

Informal description

Let $f : \alpha \to \delta \to \varepsilon$, $g : \beta \to \gamma \to \delta$, $f_1 : \alpha \to \beta \to \beta'$, $f_2 : \alpha \to \gamma \to \gamma'$, and $g' : \beta' \to \gamma' \to \varepsilon$ be functions such that for all $a \in \alpha$, $b \in \beta$, and $c \in \gamma$, the following distributive property holds: \[ f(a, g(b, c)) = g'(f_1(a, b), f_2(a, c)). \] Then, for any sets $s \subseteq \alpha$, $t \subseteq \beta$, and $u \subseteq \gamma$, we have the subset relation: \[ \text{image2}(f, s, \text{image2}(g, t, u)) \subseteq \text{image2}(g', \text{image2}(f_1, s, t), \text{image2}(f_2, s, u)). \]

Set.image2_distrib_subset_right theorem

 {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)

Full source

/-- The other direction does not hold because of the `u`-`u` cross terms on the RHS. -/
theorem image2_distrib_subset_right {f : δ → γ → ε} {g : α → β → δ} {f₁ : α → γ → α'}
    {f₂ : β → γ → β'} {g' : α' → β' → ε} (h_distrib : ∀ a b c, f (g a b) c = g' (f₁ a c) (f₂ b c)) :
    image2image2 f (image2 g s t) u ⊆ image2 g' (image2 f₁ s u) (image2 f₂ t u) := by
  rintro _ ⟨_, ⟨a, ha, b, hb, rfl⟩, c, hc, rfl⟩
  rw [h_distrib]
  exact mem_image2_of_mem (mem_image2_of_mem ha hc) (mem_image2_of_mem hb hc)

Right Distributive Property of Binary Image Sets under Function Composition

Informal description

Let $f : \delta \to \gamma \to \varepsilon$, $g : \alpha \to \beta \to \delta$, $f_1 : \alpha \to \gamma \to \alpha'$, $f_2 : \beta \to \gamma \to \beta'$, and $g' : \alpha' \to \beta' \to \varepsilon$ be functions such that for all $a \in \alpha$, $b \in \beta$, and $c \in \gamma$, the distributive property $f(g(a, b), c) = g'(f_1(a, c), f_2(b, c))$ holds. Then for any sets $s \subseteq \alpha$, $t \subseteq \beta$, and $u \subseteq \gamma$, we have the inclusion: \[ \text{image2}(f, \text{image2}(g, s, t), u) \subseteq \text{image2}(g', \text{image2}(f_1, s, u), \text{image2}(f_2, t, u)). \]

Set.image_image2_antidistrib theorem

 {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'} (h_antidistrib : ∀ a b, g (f a b) = f' (g₁ b) (g₂ a)) :
  (image2 f s t).image g = image2 f' (t.image g₁) (s.image g₂)

Full source

theorem image_image2_antidistrib {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'}
    (h_antidistrib : ∀ a b, g (f a b) = f' (g₁ b) (g₂ a)) :
    (image2 f s t).image g = image2 f' (t.image g₁) (s.image g₂) := by
  rw [image2_swap f]
  exact image_image2_distrib fun _ _ => h_antidistrib _ _

Antidistributivity of Image over Binary Image: $g(f(s, t)) = f'(g_1(t), g_2(s))$

Informal description

Let $f \colon \alpha \to \beta \to \gamma$ be a binary function, $g \colon \gamma \to \delta$ a function, and $f' \colon \beta' \to \alpha' \to \delta$ another binary function. Suppose there exist functions $g_1 \colon \beta \to \beta'$ and $g_2 \colon \alpha \to \alpha'$ such that for all $a \in \alpha$ and $b \in \beta$, the antidistributive property $g(f(a, b)) = f'(g_1(b), g_2(a))$ holds. Then for any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the binary image $\text{image2}(f, s, t)$ under $g$ equals the binary image of $g_1(t)$ and $g_2(s)$ under $f'$: \[ g(\text{image2}(f, s, t)) = \text{image2}(f', g_1(t), g_2(s)). \]

Set.image_image2_antidistrib_left theorem

 {g : γ → δ} {f' : β' → α → δ} {g' : β → β'} (h_antidistrib : ∀ a b, g (f a b) = f' (g' b) a) :
  (image2 f s t).image g = image2 f' (t.image g') s

Full source

/-- Symmetric statement to `Set.image2_image_left_anticomm`. -/
theorem image_image2_antidistrib_left {g : γ → δ} {f' : β' → α → δ} {g' : β → β'}
    (h_antidistrib : ∀ a b, g (f a b) = f' (g' b) a) :
    (image2 f s t).image g = image2 f' (t.image g') s :=
  (image_image2_antidistrib h_antidistrib).trans <| by rw [image_id']

Left Antidistributivity of Image over Binary Image: $g(f(s, t)) = f'(g'(t), s)$

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a binary function, $g : \gamma \to \delta$ a function, and $f' : \beta' \to \alpha \to \delta$ another binary function. Suppose there exists a function $g' : \beta \to \beta'$ such that for all $a \in \alpha$ and $b \in \beta$, the antidistributive property $g(f(a, b)) = f'(g'(b), a)$ holds. Then for any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the binary image $\text{image2}(f, s, t)$ under $g$ equals the binary image of $g'(t)$ and $s$ under $f'$: \[ g(\text{image2}(f, s, t)) = \text{image2}(f', g'(t), s). \]

Set.image_image2_antidistrib_right theorem

 {g : γ → δ} {f' : β → α' → δ} {g' : α → α'} (h_antidistrib : ∀ a b, g (f a b) = f' b (g' a)) :
  (image2 f s t).image g = image2 f' t (s.image g')

Full source

/-- Symmetric statement to `Set.image_image2_right_anticomm`. -/
theorem image_image2_antidistrib_right {g : γ → δ} {f' : β → α' → δ} {g' : α → α'}
    (h_antidistrib : ∀ a b, g (f a b) = f' b (g' a)) :
    (image2 f s t).image g = image2 f' t (s.image g') :=
  (image_image2_antidistrib h_antidistrib).trans <| by rw [image_id']

Right Antidistributivity of Image over Binary Image: $g(f(s, t)) = f'(t, g'(s))$

Informal description

Let $f \colon \alpha \to \beta \to \gamma$ be a binary function, $g \colon \gamma \to \delta$ a function, and $f' \colon \beta \to \alpha' \to \delta$ another binary function. Suppose there exists a function $g' \colon \alpha \to \alpha'$ such that for all $a \in \alpha$ and $b \in \beta$, the antidistributive property $g(f(a, b)) = f'(b, g'(a))$ holds. Then for any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the binary image $\text{image2}(f, s, t)$ under $g$ equals the binary image of $t$ and $g'(s)$ under $f'$: \[ g(\text{image2}(f, s, t)) = \text{image2}(f', t, g'(s)). \]

Set.image2_image_left_anticomm theorem

 {f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ} (h_left_anticomm : ∀ a b, f (g a) b = g' (f' b a)) :
  image2 f (s.image g) t = (image2 f' t s).image g'

Full source

/-- Symmetric statement to `Set.image_image2_antidistrib_left`. -/
theorem image2_image_left_anticomm {f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ}
    (h_left_anticomm : ∀ a b, f (g a) b = g' (f' b a)) :
    image2 f (s.image g) t = (image2 f' t s).image g' :=
  (image_image2_antidistrib_left fun a b => (h_left_anticomm b a).symm).symm

Left-Anticommutative Property of Binary Image Composition: $\text{image2}(f, g(s), t) = g'(\text{image2}(f', t, s))$

Informal description

Let $f \colon \alpha' \to \beta \to \gamma$ and $f' \colon \beta \to \alpha \to \delta$ be binary functions, and let $g \colon \alpha \to \alpha'$ and $g' \colon \delta \to \gamma$ be functions. Suppose that for all $a \in \alpha$ and $b \in \beta$, the left-anticommutative property $f(g(a), b) = g'(f'(b, a))$ holds. Then for any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the binary image of $g(s)$ and $t$ under $f$ equals the image of the binary image of $t$ and $s$ under $f'$ composed with $g'$: \[ \text{image2}(f, g(s), t) = g'(\text{image2}(f', t, s)). \]

Set.image_image2_right_anticomm theorem

 {f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ} (h_right_anticomm : ∀ a b, f a (g b) = g' (f' b a)) :
  image2 f s (t.image g) = (image2 f' t s).image g'

Full source

/-- Symmetric statement to `Set.image_image2_antidistrib_right`. -/
theorem image_image2_right_anticomm {f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ}
    (h_right_anticomm : ∀ a b, f a (g b) = g' (f' b a)) :
    image2 f s (t.image g) = (image2 f' t s).image g' :=
  (image_image2_antidistrib_right fun a b => (h_right_anticomm b a).symm).symm

Right Anticommutativity of Binary Image under Function Composition

Informal description

Let $f \colon \alpha \to \beta' \to \gamma$ and $f' \colon \beta \to \alpha \to \delta$ be binary functions, $g \colon \beta \to \beta'$ and $g' \colon \delta \to \gamma$ be functions. Suppose that for all $a \in \alpha$ and $b \in \beta$, the right anticommutativity condition $f(a, g(b)) = g'(f'(b, a))$ holds. Then for any subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the binary image of $s$ and $g(t)$ under $f$ equals the image of the binary image of $t$ and $s$ under $f'$ composed with $g'$: \[ \text{image2}(f, s, g(t)) = g'(\text{image2}(f', t, s)). \]

Set.image2_left_identity theorem

{f : α → β → β} {a : α} (h : ∀ b, f a b = b) (t : Set β) : image2 f { a } t = t

Full source

/-- If `a` is a left identity for `f : α → β → β`, then `{a}` is a left identity for
`Set.image2 f`. -/
lemma image2_left_identity {f : α → β → β} {a : α} (h : ∀ b, f a b = b) (t : Set β) :
    image2 f {a} t = t := by
  rw [image2_singleton_left, show f a = id from funext h, image_id]

Left Identity Property for Binary Image of Sets

Informal description

Let $f : \alpha \to \beta \to \beta$ be a binary function and $a \in \alpha$ be a left identity for $f$, i.e., $f(a, b) = b$ for all $b \in \beta$. Then for any set $t \subseteq \beta$, the image of $\{a\}$ and $t$ under $f$ equals $t$, i.e., $\{f(a, b) \mid b \in t\} = t$.

Set.image2_right_identity theorem

{f : α → β → α} {b : β} (h : ∀ a, f a b = a) (s : Set α) : image2 f s { b } = s

Full source

/-- If `b` is a right identity for `f : α → β → α`, then `{b}` is a right identity for
`Set.image2 f`. -/
lemma image2_right_identity {f : α → β → α} {b : β} (h : ∀ a, f a b = a) (s : Set α) :
    image2 f s {b} = s := by
  rw [image2_singleton_right, funext h, image_id']

Right Identity Property for Binary Image of Sets

Informal description

Let $f : \alpha \to \beta \to \alpha$ be a binary function and $b \in \beta$ be a right identity for $f$, i.e., $f(a, b) = a$ for all $a \in \alpha$. Then for any set $s \subseteq \alpha$, the image of $s$ and $\{b\}$ under $f$ equals $s$, i.e., $\{f(a, b) \mid a \in s\} = s$.

Set.image2_inter_union_subset_union theorem

: image2 f (s ∩ s') (t ∪ t') ⊆ image2 f s t ∪ image2 f s' t'

Full source

theorem image2_inter_union_subset_union :
    image2image2 f (s ∩ s') (t ∪ t') ⊆ image2 f s t ∪ image2 f s' t' := by
  rw [image2_union_right]
  exact
    union_subset_union (image2_subset_right inter_subset_left)
      (image2_subset_right inter_subset_right)

Subset Property for Binary Image on Intersection-Union Pairs

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and sets $s, s' \subseteq \alpha$, $t, t' \subseteq \beta$, the image of $f$ on $(s \cap s') \times (t \cup t')$ is a subset of the union of the images of $f$ on $s \times t$ and $s' \times t'$. That is, \[ \{f(a, b) \mid a \in s \cap s', b \in t \cup t'\} \subseteq \{f(a, b) \mid a \in s, b \in t\} \cup \{f(a, b) \mid a \in s', b \in t'\}. \]

Set.image2_union_inter_subset_union theorem

: image2 f (s ∪ s') (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t'

Full source

theorem image2_union_inter_subset_union :
    image2image2 f (s ∪ s') (t ∩ t') ⊆ image2 f s t ∪ image2 f s' t' := by
  rw [image2_union_left]
  exact
    union_subset_union (image2_subset_left inter_subset_left)
      (image2_subset_left inter_subset_right)

Subset Property of Binary Image over Union and Intersection: $\text{image2}(f, s \cup s', t \cap t') \subseteq \text{image2}(f, s, t) \cup \text{image2}(f, s', t')$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and sets $s, s' \subseteq \alpha$, $t, t' \subseteq \beta$, the image of $f$ on the union $(s \cup s') \times (t \cap t')$ is a subset of the union of the images of $f$ on $s \times t$ and $s' \times t'$. That is, \[ \{f(a, b) \mid a \in s \cup s', b \in t \cap t'\} \subseteq \{f(a, b) \mid a \in s, b \in t\} \cup \{f(a, b) \mid a \in s', b \in t'\}. \]

Set.image2_inter_union_subset theorem

{f : α → α → β} {s t : Set α} (hf : ∀ a b, f a b = f b a) : image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t

Full source

theorem image2_inter_union_subset {f : α → α → β} {s t : Set α} (hf : ∀ a b, f a b = f b a) :
    image2image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t := by
  rw [inter_comm]
  exact image2_inter_union_subset_union.trans (union_subset (image2_comm hf).subset Subset.rfl)

Commutative Binary Image Subset Property: $\text{image2}(f, s \cap t, s \cup t) \subseteq \text{image2}(f, s, t)$ for Commutative $f$

Informal description

For any binary function $f : \alpha \to \alpha \to \beta$ that is commutative (i.e., $f(a, b) = f(b, a)$ for all $a, b \in \alpha$) and any sets $s, t \subseteq \alpha$, the image of $f$ on $(s \cap t) \times (s \cup t)$ is a subset of the image of $f$ on $s \times t$. That is, \[ \{f(a, b) \mid a \in s \cap t, b \in s \cup t\} \subseteq \{f(a, b) \mid a \in s, b \in t\}. \]

Set.image2_union_inter_subset theorem

{f : α → α → β} {s t : Set α} (hf : ∀ a b, f a b = f b a) : image2 f (s ∪ t) (s ∩ t) ⊆ image2 f s t

Full source

theorem image2_union_inter_subset {f : α → α → β} {s t : Set α} (hf : ∀ a b, f a b = f b a) :
    image2image2 f (s ∪ t) (s ∩ t) ⊆ image2 f s t := by
  rw [image2_comm hf]
  exact image2_inter_union_subset hf

Commutative Binary Image Subset Property: $\text{image2}(f, s \cup t, s \cap t) \subseteq \text{image2}(f, s, t)$ for Commutative $f$

Informal description

For any commutative binary function $f : \alpha \to \alpha \to \beta$ (i.e., $f(a, b) = f(b, a)$ for all $a, b \in \alpha$) and any sets $s, t \subseteq \alpha$, the image of $f$ on $(s \cup t) \times (s \cap t)$ is a subset of the image of $f$ on $s \times t$. That is, \[ \{f(a, b) \mid a \in s \cup t, b \in s \cap t\} \subseteq \{f(a, b) \mid a \in s, b \in t\}. \]

Notes