Mathlib.Data.Finset.NAry

Finset.image₂ definition

(f : α → β → γ) (s : Finset α) (t : Finset β) : Finset γ

Full source

/-- The image of a binary function `f : α → β → γ` as a function `Finset α → Finset β → Finset γ`.
Mathematically this should be thought of as the image of the corresponding function `α × β → γ`. -/
def image₂ (f : α → β → γ) (s : Finset α) (t : Finset β) : Finset γ :=
  (s ×ˢ t).image <| uncurry f

Binary image of finite sets

Informal description

Given a binary function $ f : \alpha \to \beta \to \gamma $ and finite sets $ s \subseteq \alpha $ and $ t \subseteq \beta $, the image $ \text{image}_2(f, s, t) $ is the finite subset of $ \gamma $ consisting of all elements $ f(a, b) $ where $ a \in s $ and $ b \in t $. This can be thought of as the image of the corresponding function $ \alpha \times \beta \to \gamma $ applied to the Cartesian product $ s \times t $.

Finset.mem_image₂ theorem

: c ∈ image₂ f s t ↔ ∃ a ∈ s, ∃ b ∈ t, f a b = c

Full source

@[simp]
theorem mem_image₂ : c ∈ image₂ f s tc ∈ image₂ f s t ↔ ∃ a ∈ s, ∃ b ∈ t, f a b = c := by
  simp [image₂, and_assoc]

Membership Criterion for Binary Image of Finite Sets

Informal description

An element $c$ belongs to the binary image $\text{image}_2(f, s, t)$ of finite sets $s \subseteq \alpha$ and $t \subseteq \beta$ under a binary function $f : \alpha \to \beta \to \gamma$ if and only if there exist elements $a \in s$ and $b \in t$ such that $f(a, b) = c$.

Finset.coe_image₂ theorem

(f : α → β → γ) (s : Finset α) (t : Finset β) : (image₂ f s t : Set γ) = Set.image2 f s t

Full source

@[simp, norm_cast]
theorem coe_image₂ (f : α → β → γ) (s : Finset α) (t : Finset β) :
    (image₂ f s t : Set γ) = Set.image2 f s t :=
  Set.ext fun _ => mem_image₂

Equality of Binary Image Sets: $\text{image}_2(f, s, t) = \text{image2}(f, s, t)$

Informal description

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

Finset.card_image₂_le theorem

(f : α → β → γ) (s : Finset α) (t : Finset β) : #(image₂ f s t) ≤ #s * #t

Full source

theorem card_image₂_le (f : α → β → γ) (s : Finset α) (t : Finset β) :
    #(image₂ f s t) ≤ #s * #t :=
  card_image_le.trans_eq <| card_product _ _

Cardinality Bound for Binary Image of Finite Sets: $|\text{image}_2(f, s, t)| \leq |s| \cdot |t|$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the cardinality of the binary image $\text{image}_2(f, s, t)$ is less than or equal to the product of the cardinalities of $s$ and $t$, i.e., \[ |\text{image}_2(f, s, t)| \leq |s| \cdot |t|. \]

Finset.card_image₂_iff theorem

: #(image₂ f s t) = #s * #t ↔ (s ×ˢ t : Set (α × β)).InjOn fun x => f x.1 x.2

Full source

theorem card_image₂_iff :
    #(image₂ f s t)#(image₂ f s t) = #s * #t ↔ (s ×ˢ t : Set (α × β)).InjOn fun x => f x.1 x.2 := by
  rw [← card_product, ← coe_product]
  exact card_image_iff

Cardinality Condition for Binary Image of Finite Sets: $|\text{image}_2(f, s, t)| = |s||t| \iff f$ injective on $s \times t$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and finite sets $s \subseteq \alpha$, $t \subseteq \beta$, the cardinality of the binary image $\text{image}_2(f, s, t)$ equals the product of the cardinalities of $s$ and $t$ if and only if the function $(x,y) \mapsto f(x,y)$ is injective on the Cartesian product set $s \times t$. That is, \[ |\text{image}_2(f, s, t)| = |s| \cdot |t| \iff \text{InjOn} (\lambda (x,y), f(x,y)) (s \times t). \]

Finset.card_image₂ theorem

(hf : Injective2 f) (s : Finset α) (t : Finset β) : #(image₂ f s t) = #s * #t

Full source

theorem card_image₂ (hf : Injective2 f) (s : Finset α) (t : Finset β) :
    #(image₂ f s t) = #s * #t :=
  (card_image_of_injective _ hf.uncurry).trans <| card_product _ _

Cardinality of Binary Image of Finite Sets under Injective Function: $|\text{image}_2(f, s, t)| = |s| \cdot |t|$

Informal description

For any injective binary function $ f : \alpha \to \beta \to \gamma $ and finite sets $ s \subseteq \alpha $ and $ t \subseteq \beta $, the cardinality of the binary image $ \text{image}_2(f, s, t) $ is equal to the product of the cardinalities of $ s $ and $ t $, i.e., \[ |\text{image}_2(f, s, t)| = |s| \cdot |t|. \]

Finset.mem_image₂_of_mem theorem

(ha : a ∈ s) (hb : b ∈ t) : f a b ∈ image₂ f s t

Full source

theorem mem_image₂_of_mem (ha : a ∈ s) (hb : b ∈ t) : f a b ∈ image₂ f s t :=
  mem_image₂.2 ⟨a, ha, b, hb, rfl⟩

Membership in Binary Image via Pair Membership

Informal description

For any elements $a \in s$ and $b \in t$ in finite sets $s \subseteq \alpha$ and $t \subseteq \beta$ respectively, and for any binary function $f : \alpha \to \beta \to \gamma$, the element $f(a, b)$ belongs to the binary image $\text{image}_2(f, s, t) \subseteq \gamma$.

Finset.mem_image₂_iff theorem

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

Full source

theorem mem_image₂_iff (hf : Injective2 f) : f a b ∈ image₂ f s tf a b ∈ image₂ f s t ↔ a ∈ s ∧ b ∈ t := by
  rw [← mem_coe, coe_image₂, mem_image2_iff hf, mem_coe, mem_coe]

Characterization of Membership in Binary Image via Injectivity: $f(a,b) \in \text{image}_2(f,s,t) \leftrightarrow a \in s \land b \in t$

Informal description

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

Finset.image₂_subset theorem

(hs : s ⊆ s') (ht : t ⊆ t') : image₂ f s t ⊆ image₂ f s' t'

Full source

@[gcongr]
theorem image₂_subset (hs : s ⊆ s') (ht : t ⊆ t') : image₂image₂ f s t ⊆ image₂ f s' t' := by
  rw [← coe_subset, coe_image₂, coe_image₂]
  exact image2_subset hs ht

Monotonicity of Binary Image under Subset Inclusion for Finite Sets

Informal description

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

Finset.image₂_subset_left theorem

(ht : t ⊆ t') : image₂ f s t ⊆ image₂ f s t'

Full source

@[gcongr]
theorem image₂_subset_left (ht : t ⊆ t') : image₂image₂ f s t ⊆ image₂ f s t' :=
  image₂_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 finite sets $s \subseteq \alpha$, $t, t' \subseteq \beta$, if $t \subseteq t'$, then the binary image $\text{image}_2(f, s, t)$ is a subset of $\text{image}_2(f, s, t')$.

Finset.image₂_subset_right theorem

(hs : s ⊆ s') : image₂ f s t ⊆ image₂ f s' t

Full source

@[gcongr]
theorem image₂_subset_right (hs : s ⊆ s') : image₂image₂ f s t ⊆ image₂ f s' t :=
  image₂_subset hs Subset.rfl

Right Monotonicity of Binary Image under Subset Inclusion for Finite Sets

Informal description

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

Finset.image_subset_image₂_left theorem

(hb : b ∈ t) : s.image (fun a => f a b) ⊆ image₂ f s t

Full source

theorem image_subset_image₂_left (hb : b ∈ t) : s.image (fun a => f a b) ⊆ image₂ f s t :=
  image_subset_iff.2 fun _ ha => mem_image₂_of_mem ha hb

Left Image Subset of Binary Image for Fixed Right Element

Informal description

For any element $b \in t$ in a finite set $t \subseteq \beta$, the image of a finite set $s \subseteq \alpha$ under the function $a \mapsto f(a, b)$ is a subset of the binary image $\text{image}_2(f, s, t) \subseteq \gamma$.

Finset.image_subset_image₂_right theorem

(ha : a ∈ s) : t.image (fun b => f a b) ⊆ image₂ f s t

Full source

theorem image_subset_image₂_right (ha : a ∈ s) : t.image (fun b => f a b) ⊆ image₂ f s t :=
  image_subset_iff.2 fun _ => mem_image₂_of_mem ha

Right Image Subset of Binary Image for Fixed Left Element

Informal description

For any element $a$ in a finite set $s \subseteq \alpha$, and for any finite set $t \subseteq \beta$, the image of $t$ under the function $\lambda b, f(a, b)$ is a subset of the binary image $\text{image}_2(f, s, t) \subseteq \gamma$.

Finset.forall_mem_image₂ theorem

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

Full source

lemma forall_mem_image₂ {p : γ → Prop} :
    (∀ z ∈ image₂ f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y) := by
  simp_rw [← mem_coe, coe_image₂, forall_mem_image2]

Universal Property of Binary Image on Finite Sets

Informal description

For any predicate $p : \gamma \to \mathrm{Prop}$, the following equivalence holds: $(\forall z \in \mathrm{image}_2(f, s, t), p(z)) \leftrightarrow (\forall x \in s, \forall y \in t, p(f(x, y)))$. In other words, a property $p$ holds for all elements of the binary image $\mathrm{image}_2(f, s, t)$ if and only if $p$ holds for $f(x, y)$ for all $x \in s$ and $y \in t$.

Finset.exists_mem_image₂ theorem

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

Full source

lemma exists_mem_image₂ {p : γ → Prop} :
    (∃ z ∈ image₂ f s t, p z) ↔ ∃ x ∈ s, ∃ y ∈ t, p (f x y) := by
  simp_rw [← mem_coe, coe_image₂, exists_mem_image2]

Existence Criterion for Binary Image of Finite Sets

Informal description

For any predicate $p : \gamma \to \mathrm{Prop}$, there exists an element $z$ in the binary image $\text{image}_2(f, s, t)$ such that $p(z)$ holds if and only if there exist elements $x \in s$ and $y \in t$ such that $p(f(x, y))$ holds.

Finset.image₂_subset_iff theorem

: image₂ f s t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u

Full source

@[simp]
theorem image₂_subset_iff : image₂image₂ f s t ⊆ uimage₂ f s t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u :=
  forall_mem_image₂

Subset Criterion for Binary Image of Finite Sets

Informal description

For a binary function $f : \alpha \to \beta \to \gamma$, finite sets $s \subseteq \alpha$, $t \subseteq \beta$, and $u \subseteq \gamma$, the binary image $\mathrm{image}_2(f, s, t)$ is a subset of $u$ if and only if for every $x \in s$ and $y \in t$, we have $f(x, y) \in u$.

Finset.image₂_subset_iff_left theorem

: image₂ f s t ⊆ u ↔ ∀ a ∈ s, (t.image fun b => f a b) ⊆ u

Full source

theorem image₂_subset_iff_left : image₂image₂ f s t ⊆ uimage₂ f s t ⊆ u ↔ ∀ a ∈ s, (t.image fun b => f a b) ⊆ u := by
  simp_rw [image₂_subset_iff, image_subset_iff]

Left Partial Image Subset Criterion for Binary Image of Finite Sets

Informal description

For a binary function $f : \alpha \to \beta \to \gamma$ and finite sets $s \subseteq \alpha$, $t \subseteq \beta$, and $u \subseteq \gamma$, the binary image $\text{image}_2(f, s, t)$ is a subset of $u$ if and only if for every element $a \in s$, the image of $t$ under the partial application $f(a, \cdot)$ is a subset of $u$.

Finset.image₂_subset_iff_right theorem

: image₂ f s t ⊆ u ↔ ∀ b ∈ t, (s.image fun a => f a b) ⊆ u

Full source

theorem image₂_subset_iff_right : image₂image₂ f s t ⊆ uimage₂ f s t ⊆ u ↔ ∀ b ∈ t, (s.image fun a => f a b) ⊆ u := by
  simp_rw [image₂_subset_iff, image_subset_iff, @forall₂_swap α]

Right Subset Condition for Binary Image of Finite Sets

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$, finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, and a finite set $u \subseteq \gamma$, the following are equivalent: 1. The binary image $\text{image}_2(f, s, t)$ is a subset of $u$. 2. For every element $b \in t$, the image of $s$ under the function $\lambda a, f(a, b)$ is a subset of $u$. In other words, $\text{image}_2(f, s, t) \subseteq u$ if and only if for every $b \in t$, we have $\{f(a, b) \mid a \in s\} \subseteq u$.

Finset.image₂_nonempty_iff theorem

: (image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Full source

@[simp]
theorem image₂_nonempty_iff : (image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty := by
  rw [← coe_nonempty, coe_image₂]
  exact image2_nonempty_iff

Nonempty Binary Image of Finite Sets iff Both Sets Nonempty

Informal description

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

Finset.Nonempty.image₂ theorem

(hs : s.Nonempty) (ht : t.Nonempty) : (image₂ f s t).Nonempty

Full source

@[aesop safe apply (rule_sets := [finsetNonempty])]
theorem Nonempty.image₂ (hs : s.Nonempty) (ht : t.Nonempty) : (image₂ f s t).Nonempty :=
  image₂_nonempty_iff.2 ⟨hs, ht⟩

Nonempty Binary Image of Nonempty Finite Sets

Informal description

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

Finset.Nonempty.of_image₂_left theorem

(h : (s.image₂ f t).Nonempty) : s.Nonempty

Full source

theorem Nonempty.of_image₂_left (h : (s.image₂ f t).Nonempty) : s.Nonempty :=
  (image₂_nonempty_iff.1 h).1

Nonemptiness of Left Set in Nonempty Binary Image of Finite Sets

Informal description

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

Finset.Nonempty.of_image₂_right theorem

(h : (s.image₂ f t).Nonempty) : t.Nonempty

Full source

theorem Nonempty.of_image₂_right (h : (s.image₂ f t).Nonempty) : t.Nonempty :=
  (image₂_nonempty_iff.1 h).2

Nonempty Right Set from Nonempty Binary Image

Informal description

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

Finset.image₂_empty_left theorem

: image₂ f ∅ t = ∅

Full source

@[simp]
theorem image₂_empty_left : image₂ f ∅ t = ∅ :=
  coe_injective <| by simp

Empty Left Set Yields Empty Binary Image for Finite Sets

Informal description

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

Finset.image₂_empty_right theorem

: image₂ f s ∅ = ∅

Full source

@[simp]
theorem image₂_empty_right : image₂ f s ∅ = ∅ :=
  coe_injective <| by simp

Empty Right Set Yields Empty Binary Image

Informal description

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

Finset.image₂_eq_empty_iff theorem

: image₂ f s t = ∅ ↔ s = ∅ ∨ t = ∅

Full source

@[simp]
theorem image₂_eq_empty_iff : image₂image₂ f s t = ∅ ↔ s = ∅ ∨ t = ∅ := by
  simp_rw [← not_nonempty_iff_eq_empty, image₂_nonempty_iff, not_and_or]

Empty Binary Image Criterion for Finite Sets

Informal description

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

Finset.image₂_singleton_left theorem

: image₂ f { a } t = t.image fun b => f a b

Full source

@[simp]
theorem image₂_singleton_left : image₂ f {a} t = t.image fun b => f a b :=
  ext fun x => by simp

Binary image of singleton left set equals image of function application

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$, any element $a \in \alpha$, and any finite set $t \subseteq \beta$, the binary image $\text{image}_2(f, \{a\}, t)$ is equal to the image of the function $f(a, \cdot)$ applied to $t$, i.e., $\{f(a, b) \mid b \in t\}$.

Finset.image₂_singleton_right theorem

: image₂ f s { b } = s.image fun a => f a b

Full source

@[simp]
theorem image₂_singleton_right : image₂ f s {b} = s.image fun a => f a b :=
  ext fun x => by simp

Binary image of a finite set with a singleton equals unary image of pointwise application

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$, finite set $s \subseteq \alpha$, and singleton set $\{b\} \subseteq \beta$, the binary image $\text{image}_2(f, s, \{b\})$ is equal to the image of the function $\lambda a, f(a, b)$ applied to $s$.

Finset.image₂_singleton_left' theorem

: image₂ f { a } t = t.image (f a)

Full source

theorem image₂_singleton_left' : image₂ f {a} t = t.image (f a) :=
  image₂_singleton_left

Binary image of singleton left set equals unary image of partial application

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$, any element $a \in \alpha$, and any finite set $t \subseteq \beta$, the binary image $\text{image}_2(f, \{a\}, t)$ is equal to the image of the function $f(a, \cdot)$ applied to $t$.

Finset.image₂_singleton theorem

: image₂ f { a } { b } = {f a b}

Full source

theorem image₂_singleton : image₂ f {a} {b} = {f a b} := by simp

Binary image of singletons equals singleton of image

Informal description

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

Finset.image₂_union_left theorem

[DecidableEq α] : image₂ f (s ∪ s') t = image₂ f s t ∪ image₂ f s' t

Full source

theorem image₂_union_left [DecidableEq α] : image₂ f (s ∪ s') t = image₂image₂ f s t ∪ image₂ f s' t :=
  coe_injective <| by
    push_cast
    exact image2_union_left

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

Informal description

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

Finset.image₂_union_right theorem

[DecidableEq β] : image₂ f s (t ∪ t') = image₂ f s t ∪ image₂ f s t'

Full source

theorem image₂_union_right [DecidableEq β] : image₂ f s (t ∪ t') = image₂image₂ f s t ∪ image₂ f s t' :=
  coe_injective <| by
    push_cast
    exact image2_union_right

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

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and finite sets $s \subseteq \alpha$, $t, t' \subseteq \beta$, the binary image of $f$ over $s$ and the union $t \cup t'$ is equal to the union of the binary images of $f$ over $s$ and $t$ and over $s$ and $t'$. That is, \[ \text{image}_2(f, s, t \cup t') = \text{image}_2(f, s, t) \cup \text{image}_2(f, s, t'). \]

Finset.image₂_insert_left theorem

[DecidableEq α] : image₂ f (insert a s) t = (t.image fun b => f a b) ∪ image₂ f s t

Full source

@[simp]
theorem image₂_insert_left [DecidableEq α] :
    image₂ f (insert a s) t = (t.image fun b => f a b) ∪ image₂ f s t :=
  coe_injective <| by
    push_cast
    exact image2_insert_left

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

Informal description

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

Finset.image₂_insert_right theorem

[DecidableEq β] : image₂ f s (insert b t) = (s.image fun a => f a b) ∪ image₂ f s t

Full source

@[simp]
theorem image₂_insert_right [DecidableEq β] :
    image₂ f s (insert b t) = (s.image fun a => f a b) ∪ image₂ f s t :=
  coe_injective <| by
    push_cast
    exact image2_insert_right

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

Informal description

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

Finset.image₂_inter_left theorem

[DecidableEq α] (hf : Injective2 f) : image₂ f (s ∩ s') t = image₂ f s t ∩ image₂ f s' t

Full source

theorem image₂_inter_left [DecidableEq α] (hf : Injective2 f) :
    image₂ f (s ∩ s') t = image₂image₂ f s t ∩ image₂ f s' t :=
  coe_injective <| by
    push_cast
    exact image2_inter_left hf

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

Informal description

For any injective binary function $f : \alpha \to \beta \to \gamma$ and finite sets $s, s' \subseteq \alpha$, $t \subseteq \beta$, the binary image of $f$ on the intersection $s \cap s'$ and $t$ equals the intersection of the binary images of $f$ on $s$ and $t$ and on $s'$ and $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\}. \]

Finset.image₂_inter_right theorem

[DecidableEq β] (hf : Injective2 f) : image₂ f s (t ∩ t') = image₂ f s t ∩ image₂ f s t'

Full source

theorem image₂_inter_right [DecidableEq β] (hf : Injective2 f) :
    image₂ f s (t ∩ t') = image₂image₂ f s t ∩ image₂ f s t' :=
  coe_injective <| by
    push_cast
    exact image2_inter_right hf

Binary Image Distributes over Right Intersection for Injective Functions: $\text{image}_2(f, s, t \cap t') = \text{image}_2(f, s, t) \cap \text{image}_2(f, s, t')$

Informal description

For any injective binary function $f : \alpha \to \beta \to \gamma$ and finite sets $s \subseteq \alpha$, $t, t' \subseteq \beta$, the binary image of $f$ over $s$ and the intersection $t \cap t'$ is equal to the intersection of the binary images of $f$ over $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'\}. \]

Finset.image₂_inter_subset_left theorem

[DecidableEq α] : image₂ f (s ∩ s') t ⊆ image₂ f s t ∩ image₂ f s' t

Full source

theorem image₂_inter_subset_left [DecidableEq α] :
    image₂image₂ f (s ∩ s') t ⊆ image₂ f s t ∩ image₂ f s' t :=
  coe_subset.1 <| by
    push_cast
    exact image2_inter_subset_left

Left Intersection Subset Property for Binary Image of Finite Sets: $\text{image}_2(f, s \cap s', t) \subseteq \text{image}_2(f, s, t) \cap \text{image}_2(f, s', t)$

Informal description

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

Finset.image₂_inter_subset_right theorem

[DecidableEq β] : image₂ f s (t ∩ t') ⊆ image₂ f s t ∩ image₂ f s t'

Full source

theorem image₂_inter_subset_right [DecidableEq β] :
    image₂image₂ f s (t ∩ t') ⊆ image₂ f s t ∩ image₂ f s t' :=
  coe_subset.1 <| by
    push_cast
    exact image2_inter_subset_right

Subset Property of Binary Image under Right Intersection: $\text{image}_2(f, s, t \cap t') \subseteq \text{image}_2(f, s, t) \cap \text{image}_2(f, s, t')$

Informal description

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

Finset.image₂_congr theorem

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

Full source

theorem image₂_congr (h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b) : image₂ f s t = image₂ f' s t :=
  coe_injective <| by
    push_cast
    exact image2_congr h

Congruence of Binary Image under Pointwise Equality for Finite Sets

Informal description

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

Finset.image₂_congr' theorem

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

Full source

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

Equality of Binary Images under Globally Equal Functions

Informal description

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

Finset.card_image₂_singleton_left theorem

(hf : Injective (f a)) : #(image₂ f { a } t) = #t

Full source

theorem card_image₂_singleton_left (hf : Injective (f a)) : #(image₂ f {a} t) = #t := by
  rw [image₂_singleton_left, card_image_of_injective _ hf]

Cardinality of Binary Image with Singleton Left Set under Injective Function

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$, any element $a \in \alpha$, and any finite set $t \subseteq \beta$, if the function $f(a, \cdot) : \beta \to \gamma$ is injective, then the cardinality of the binary image $\text{image}_2(f, \{a\}, t)$ equals the cardinality of $t$.

Finset.card_image₂_singleton_right theorem

(hf : Injective fun a => f a b) : #(image₂ f s { b }) = #s

Full source

theorem card_image₂_singleton_right (hf : Injective fun a => f a b) :
    #(image₂ f s {b}) = #s := by rw [image₂_singleton_right, card_image_of_injective _ hf]

Cardinality Preservation in Binary Image with Singleton Right Set under Injective Function

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$, any finite set $s \subseteq \alpha$, and any element $b \in \beta$, if the function $\lambda a, f(a, b)$ is injective, then the cardinality of the binary image $\text{image}_2(f, s, \{b\})$ equals the cardinality of $s$.

Finset.image₂_singleton_inter theorem

 [DecidableEq β] (t₁ t₂ : Finset β) (hf : Injective (f a)) :
  image₂ f { a } (t₁ ∩ t₂) = image₂ f { a } t₁ ∩ image₂ f { a } t₂

Full source

theorem image₂_singleton_inter [DecidableEq β] (t₁ t₂ : Finset β) (hf : Injective (f a)) :
    image₂ f {a} (t₁ ∩ t₂) = image₂image₂ f {a} t₁ ∩ image₂ f {a} t₂ := by
  simp_rw [image₂_singleton_left, image_inter _ _ hf]

Binary Image Preserves Intersection with Singleton Left Set under Injective Function

Informal description

Let $\beta$ be a type with decidable equality, and let $f : \alpha \to \beta \to \gamma$ be a binary function. For any element $a \in \alpha$ and finite sets $t_1, t_2 \subseteq \beta$, if the function $f(a, \cdot) : \beta \to \gamma$ is injective, then the binary image of $\{a\}$ and the intersection $t_1 \cap t_2$ under $f$ equals the intersection of the binary images of $\{a\}$ with $t_1$ and $t_2$ respectively. That is, \[ \text{image}_2(f, \{a\}, t_1 \cap t_2) = \text{image}_2(f, \{a\}, t_1) \cap \text{image}_2(f, \{a\}, t_2). \]

Finset.image₂_inter_singleton theorem

 [DecidableEq α] (s₁ s₂ : Finset α) (hf : Injective fun a => f a b) :
  image₂ f (s₁ ∩ s₂) { b } = image₂ f s₁ { b } ∩ image₂ f s₂ { b }

Full source

theorem image₂_inter_singleton [DecidableEq α] (s₁ s₂ : Finset α) (hf : Injective fun a => f a b) :
    image₂ f (s₁ ∩ s₂) {b} = image₂image₂ f s₁ {b} ∩ image₂ f s₂ {b} := by
  simp_rw [image₂_singleton_right, image_inter _ _ hf]

Binary Image of Intersection with Singleton Equals Intersection of Binary Images under Injective Condition

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality on $\alpha$, and let $f : \alpha \to \beta \to \gamma$ be a binary function such that for a fixed $b \in \beta$, the function $\lambda a, f(a, b)$ is injective. For any finite sets $s_1, s_2 \subseteq \alpha$, the binary image of their intersection with the singleton $\{b\}$ equals the intersection of their binary images with $\{b\}$, i.e., \[ \text{image}_2(f, s_1 \cap s_2, \{b\}) = \text{image}_2(f, s_1, \{b\}) \cap \text{image}_2(f, s_2, \{b\}). \]

Finset.card_le_card_image₂_left theorem

{s : Finset α} (hs : s.Nonempty) (hf : ∀ a, Injective (f a)) : #t ≤ #(image₂ f s t)

Full source

theorem card_le_card_image₂_left {s : Finset α} (hs : s.Nonempty) (hf : ∀ a, Injective (f a)) :
    #t ≤ #(image₂ f s t) := by
  obtain ⟨a, ha⟩ := hs
  rw [← card_image₂_singleton_left _ (hf a)]
  exact card_le_card (image₂_subset_right <| singleton_subset_iff.2 ha)

Cardinality Lower Bound for Binary Image with Left Injective Function

Informal description

For any nonempty finite set $s \subseteq \alpha$ and any finite set $t \subseteq \beta$, if for every $a \in s$ the function $f(a, \cdot) : \beta \to \gamma$ is injective, then the cardinality of $t$ is less than or equal to the cardinality of the binary image $\text{image}_2(f, s, t)$.

Finset.card_le_card_image₂_right theorem

{t : Finset β} (ht : t.Nonempty) (hf : ∀ b, Injective fun a => f a b) : #s ≤ #(image₂ f s t)

Full source

theorem card_le_card_image₂_right {t : Finset β} (ht : t.Nonempty)
    (hf : ∀ b, Injective fun a => f a b) : #s ≤ #(image₂ f s t) := by
  obtain ⟨b, hb⟩ := ht
  rw [← card_image₂_singleton_right _ (hf b)]
  exact card_le_card (image₂_subset_left <| singleton_subset_iff.2 hb)

Cardinality Lower Bound for Binary Image with Right Injective Function

Informal description

For any nonempty finite set $t \subseteq \beta$ and any finite set $s \subseteq \alpha$, if for every $b \in t$ the function $\lambda a, f(a, b)$ is injective, then the cardinality of $s$ is less than or equal to the cardinality of the binary image $\text{image}_2(f, s, t)$.

Finset.biUnion_image_left theorem

: (s.biUnion fun a => t.image <| f a) = image₂ f s t

Full source

theorem biUnion_image_left : (s.biUnion fun a => t.image <| f a) = image₂ f s t :=
  coe_injective <| by
    push_cast
    exact Set.iUnion_image_left _

Union of Images Equals Binary Image for Finite Sets

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and finite sets $s \subseteq \alpha$, $t \subseteq \beta$, the finite union over $a \in s$ of the images $t.\text{image}(f(a))$ equals the binary image $\text{image}_2(f, s, t)$. In other words: \[ \bigcup_{a \in s} \{f(a, b) \mid b \in t\} = \{f(a, b) \mid a \in s, b \in t\} \]

Finset.biUnion_image_right theorem

: (t.biUnion fun b => s.image fun a => f a b) = image₂ f s t

Full source

theorem biUnion_image_right : (t.biUnion fun b => s.image fun a => f a b) = image₂ f s t :=
  coe_injective <| by
    push_cast
    exact Set.iUnion_image_right _

Equality of Finite Union of Right Images and Binary Image

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and finite sets $s \subseteq \alpha$, $t \subseteq \beta$, the finite union over $b \in t$ of the images $\{f(a, b) \mid a \in s\}$ equals the binary image $\text{image}_2(f, s, t)$. In other words: \[ \bigcup_{b \in t} \{f(a, b) \mid a \in s\} = \text{image}_2(f, s, t) \]

Finset.image_image₂ theorem

(f : α → β → γ) (g : γ → δ) : (image₂ f s t).image g = image₂ (fun a b => g (f a b)) s t

Full source

theorem image_image₂ (f : α → β → γ) (g : γ → δ) :
    (image₂ f s t).image g = image₂ (fun a b => g (f a b)) s t :=
  coe_injective <| by
    push_cast
    exact image_image2 _ _

Image of Binary Image Equals Binary Image of Composition for Finite Sets

Informal description

For any binary function $f \colon \alpha \to \beta \to \gamma$, any function $g \colon \gamma \to \delta$, and any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the binary image $\text{image}_2(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{image}_2(f, s, t)) = \text{image}_2(\lambda a b, g(f(a, b)), s, t). \]

Finset.image₂_image_left theorem

(f : γ → β → δ) (g : α → γ) : image₂ f (s.image g) t = image₂ (fun a b => f (g a) b) s t

Full source

theorem image₂_image_left (f : γ → β → δ) (g : α → γ) :
    image₂ f (s.image g) t = image₂ (fun a b => f (g a) b) s t :=
  coe_injective <| by
    push_cast
    exact image2_image_left _ _

Left Composition Property of Binary Image for Finite Sets: $\text{image}_2(f, g(s), t) = \text{image}_2(f \circ g, s, t)$

Informal description

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

Finset.image₂_image_right theorem

(f : α → γ → δ) (g : β → γ) : image₂ f s (t.image g) = image₂ (fun a b => f a (g b)) s t

Full source

theorem image₂_image_right (f : α → γ → δ) (g : β → γ) :
    image₂ f s (t.image g) = image₂ (fun a b => f a (g b)) s t :=
  coe_injective <| by
    push_cast
    exact image2_image_right _ _

Right Composition Property of Binary Image for Finite Sets: $\text{image}_2(f, s, g(t)) = \text{image}_2(f \circ (\text{id} \times g), s, t)$

Informal description

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

Finset.image₂_mk_eq_product theorem

[DecidableEq α] [DecidableEq β] (s : Finset α) (t : Finset β) : image₂ Prod.mk s t = s ×ˢ t

Full source

@[simp]
theorem image₂_mk_eq_product [DecidableEq α] [DecidableEq β] (s : Finset α) (t : Finset β) :
    image₂ Prod.mk s t = s ×ˢ t := by ext; simp [Prod.ext_iff]

Binary Image of Pairing Function Equals Cartesian Product for Finite Sets

Informal description

For any finite sets $s$ in type $\alpha$ and $t$ in type $\beta$ (with decidable equality on both types), the binary image of the pairing function $\text{Prod.mk}$ applied to $s$ and $t$ is equal to their Cartesian product $s \timesˢ t$. In other words, $\text{image}_2(\text{Prod.mk}, s, t) = s \timesˢ t$.

Finset.image₂_curry theorem

(f : α × β → γ) (s : Finset α) (t : Finset β) : image₂ (curry f) s t = (s ×ˢ t).image f

Full source

@[simp]
theorem image₂_curry (f : α × β → γ) (s : Finset α) (t : Finset β) :
    image₂ (curry f) s t = (s ×ˢ t).image f := rfl

Equality between Binary Image of Curried Function and Image of Cartesian Product

Informal description

Let $f : \alpha \times \beta \to \gamma$ be a function, and let $s$ and $t$ be finite subsets of $\alpha$ and $\beta$ respectively. Then the binary image of $s$ and $t$ under the curried function $\text{curry}(f) : \alpha \to \beta \to \gamma$ is equal to the image of the Cartesian product $s \times t$ under $f$. In symbols: \[ \text{image}_2(\text{curry}(f), s, t) = \text{image}(f, s \times t). \]

Finset.image_uncurry_product theorem

(f : α → β → γ) (s : Finset α) (t : Finset β) : (s ×ˢ t).image (uncurry f) = image₂ f s t

Full source

@[simp]
theorem image_uncurry_product (f : α → β → γ) (s : Finset α) (t : Finset β) :
    (s ×ˢ t).image (uncurry f) = image₂ f s t := rfl

Equivalence of Binary Image and Cartesian Product Image via Uncurrying

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and finite sets $s \subseteq \alpha$, $t \subseteq \beta$, the image of the uncurried function $f$ applied to the Cartesian product $s \times t$ equals the binary image of $f$ applied to $s$ and $t$. That is, $$ \text{image}(\text{uncurry}\, f, s \times t) = \text{image}_2(f, s, t). $$

Finset.image₂_swap theorem

(f : α → β → γ) (s : Finset α) (t : Finset β) : image₂ f s t = image₂ (fun a b => f b a) t s

Full source

theorem image₂_swap (f : α → β → γ) (s : Finset α) (t : Finset β) :
    image₂ f s t = image₂ (fun a b => f b a) t s :=
  coe_injective <| by
    push_cast
    exact image2_swap _ _ _

Commutativity of Binary Image for Finite Sets: $\text{image}_2(f, s, t) = \text{image}_2(f \circ \text{swap}, t, s)$

Informal description

For any binary function $f \colon \alpha \to \beta \to \gamma$ and finite sets $s \subseteq \alpha$, $t \subseteq \beta$, the binary image $\text{image}_2(f, s, t)$ is equal to $\text{image}_2(\lambda a b, f b a, t, s)$. That is, \[ \{f(a, b) \mid a \in s, b \in t\} = \{f(b, a) \mid a \in t, b \in s\}. \]

Finset.image₂_left theorem

[DecidableEq α] (h : t.Nonempty) : image₂ (fun x _ => x) s t = s

Full source

@[simp]
theorem image₂_left [DecidableEq α] (h : t.Nonempty) : image₂ (fun x _ => x) s t = s :=
  coe_injective <| by
    push_cast
    exact image2_left h

Left Projection Preserves Finite Set Under Binary Image with Nonempty Condition

Informal description

For any finite set $s$ of type $\alpha$ and nonempty finite set $t$ of type $\beta$, the binary image of the left projection function $\lambda x \_, x$ over $s$ and $t$ equals $s$. That is, \[ \text{image}_2(\lambda x \_, x, s, t) = s. \]

Finset.image₂_right theorem

[DecidableEq β] (h : s.Nonempty) : image₂ (fun _ y => y) s t = t

Full source

@[simp]
theorem image₂_right [DecidableEq β] (h : s.Nonempty) : image₂ (fun _ y => y) s t = t :=
  coe_injective <| by
    push_cast
    exact image2_right h

Right Projection Image of Nonempty Finite Set Equals Second Argument

Informal description

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

Finset.image₂_assoc theorem

 {γ : Type*} {u : Finset γ} {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'}
  (h_assoc : ∀ a b c, f (g a b) c = f' a (g' b c)) : image₂ f (image₂ g s t) u = image₂ f' s (image₂ g' t u)

Full source

theorem image₂_assoc {γ : Type*} {u : Finset γ}
    {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε}
    {g' : β → γ → ε'} (h_assoc : ∀ a b c, f (g a b) c = f' a (g' b c)) :
    image₂ f (image₂ g s t) u = image₂ f' s (image₂ g' t u) :=
  coe_injective <| by
    push_cast
    exact image2_assoc h_assoc

Associativity of Binary Image Operation on Finite Sets

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 finite sets $s \subseteq \alpha$, $t \subseteq \beta$, and $u \subseteq \gamma$, we have: \[ \text{image}_2(f, \text{image}_2(g, s, t), u) = \text{image}_2(f', s, \text{image}_2(g', t, u)). \]

Finset.image₂_comm theorem

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

Full source

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

Commutativity of Binary Image Operation on Finite Sets: $\text{image}_2(f, s, t) = \text{image}_2(g, t, s)$ when $f$ and $g$ are related by $f(a,b) = g(b,a)$

Informal description

For any binary function $f \colon \alpha \to \beta \to \gamma$ and finite sets $s \subseteq \alpha$, $t \subseteq \beta$, if there exists a function $g \colon \beta \to \alpha \to \gamma$ such that $f(a,b) = g(b,a)$ for all $a \in \alpha$ and $b \in \beta$, then the binary image $\text{image}_2(f, s, t)$ is equal to $\text{image}_2(g, t, s)$. That is, \[ \{f(a, b) \mid a \in s, b \in t\} = \{g(b, a) \mid b \in t, a \in s\}. \]

Finset.image₂_left_comm theorem

 {γ : Type*} {u : Finset γ} {f : α → δ → ε} {g : β → γ → δ} {f' : α → γ → δ'} {g' : β → δ' → ε}
  (h_left_comm : ∀ a b c, f a (g b c) = g' b (f' a c)) : image₂ f s (image₂ g t u) = image₂ g' t (image₂ f' s u)

Full source

theorem image₂_left_comm {γ : Type*} {u : Finset γ} {f : α → δ → ε} {g : β → γ → δ}
    {f' : α → γ → δ'} {g' : β → δ' → ε} (h_left_comm : ∀ a b c, f a (g b c) = g' b (f' a c)) :
    image₂ f s (image₂ g t u) = image₂ g' t (image₂ f' s u) :=
  coe_injective <| by
    push_cast
    exact image2_left_comm h_left_comm

Left-commutativity of binary image operation on finite sets

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 finite sets $s \subseteq \alpha$, $t \subseteq \beta$, and $u \subseteq \gamma$, we have: \[ \text{image}_2(f, s, \text{image}_2(g, t, u)) = \text{image}_2(g', t, \text{image}_2(f', s, u)). \]

Finset.image₂_right_comm theorem

 {γ : Type*} {u : Finset γ} {f : δ → γ → ε} {g : α → β → δ} {f' : α → γ → δ'} {g' : δ' → β → ε}
  (h_right_comm : ∀ a b c, f (g a b) c = g' (f' a c) b) : image₂ f (image₂ g s t) u = image₂ g' (image₂ f' s u) t

Full source

theorem image₂_right_comm {γ : Type*} {u : Finset γ} {f : δ → γ → ε} {g : α → β → δ}
    {f' : α → γ → δ'} {g' : δ' → β → ε} (h_right_comm : ∀ a b c, f (g a b) c = g' (f' a c) b) :
    image₂ f (image₂ g s t) u = image₂ g' (image₂ f' s u) t :=
  coe_injective <| by
    push_cast
    exact image2_right_comm h_right_comm

Right Commutativity of Binary Image Operation on Finite Sets

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 finite sets $s \subseteq \alpha$, $t \subseteq \beta$, and $u \subseteq \gamma$, we have: \[ \text{image}_2(f, \text{image}_2(g, s, t), u) = \text{image}_2(g', \text{image}_2(f', s, u), t). \]

Finset.image₂_image₂_image₂_comm theorem

 {γ δ : Type*} {u : Finset γ} {v : Finset δ} [DecidableEq ζ] [DecidableEq ζ'] [DecidableEq ν] {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)) :
  image₂ f (image₂ g s t) (image₂ h u v) = image₂ f' (image₂ g' s u) (image₂ h' t v)

Full source

theorem image₂_image₂_image₂_comm {γ δ : Type*} {u : Finset γ} {v : Finset δ} [DecidableEq ζ]
    [DecidableEq ζ'] [DecidableEq ν] {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)) :
    image₂ f (image₂ g s t) (image₂ h u v) = image₂ f' (image₂ g' s u) (image₂ h' t v) :=
  coe_injective <| by
    push_cast
    exact image2_image2_image2_comm h_comm

Commutativity of Nested Binary Images of Finite Sets: $\text{image}_2(f, \text{image}_2(g, s, t), \text{image}_2(h, u, v)) = \text{image}_2(f', \text{image}_2(g', s, u), \text{image}_2(h', t, v))$

Informal description

Let $\alpha, \beta, \gamma, \delta, \varepsilon, \zeta, \nu, \varepsilon', \zeta'$ be types, and 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 finite sets $s \subseteq \alpha$, $t \subseteq \beta$, $u \subseteq \gamma$, $v \subseteq \delta$, we have: $$\text{image}_2\ f\ (\text{image}_2\ g\ s\ t)\ (\text{image}_2\ h\ u\ v) = \text{image}_2\ f'\ (\text{image}_2\ g'\ s\ u)\ (\text{image}_2\ h'\ t\ v).$$

Finset.image_image₂_distrib theorem

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

Full source

theorem image_image₂_distrib {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'}
    (h_distrib : ∀ a b, g (f a b) = f' (g₁ a) (g₂ b)) :
    (image₂ f s t).image g = image₂ f' (s.image g₁) (t.image g₂) :=
  coe_injective <| by
    push_cast
    exact image_image2_distrib h_distrib

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

Informal description

Let $f \colon \alpha \times \beta \to \gamma$ be a binary function, $g \colon \gamma \to \delta$ a function, and $f' \colon \alpha' \times \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 finite subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the binary image $\text{image}_2(f, s, t)$ under $g$ equals the binary image of $g_1(s)$ and $g_2(t)$ under $f'$: \[ g(\text{image}_2(f, s, t)) = \text{image}_2(f', g_1(s), g_2(t)). \]

Finset.image_image₂_distrib_left theorem

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

Full source

/-- Symmetric statement to `Finset.image₂_image_left_comm`. -/
theorem image_image₂_distrib_left {g : γ → δ} {f' : α' → β → δ} {g' : α → α'}
    (h_distrib : ∀ a b, g (f a b) = f' (g' a) b) :
    (image₂ f s t).image g = image₂ f' (s.image g') t :=
  coe_injective <| by
    push_cast
    exact image_image2_distrib_left h_distrib

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

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a binary function, $g : \gamma \to \delta$ a function, and $f' : \alpha' \to \beta \to \delta$ another binary function. Suppose there exists a function $g' : \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 finite subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the binary image $\text{image}_2(f, s, t)$ under $g$ equals the binary image of $g'(s)$ and $t$ under $f'$: \[ g(\text{image}_2(f, s, t)) = \text{image}_2(f', g'(s), t). \]

Finset.image_image₂_distrib_right theorem

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

Full source

/-- Symmetric statement to `Finset.image_image₂_right_comm`. -/
theorem image_image₂_distrib_right {g : γ → δ} {f' : α → β' → δ} {g' : β → β'}
    (h_distrib : ∀ a b, g (f a b) = f' a (g' b)) :
    (image₂ f s t).image g = image₂ f' s (t.image g') :=
  coe_injective <| by
    push_cast
    exact image_image2_distrib_right h_distrib

Right Distributivity of Image over Binary Image for Finite Sets: $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 finite subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the binary image $\text{image}_2(f, s, t)$ under $g$ equals the binary image of $s$ and $g'(t)$ under $f'$: \[ g(\text{image}_2(f, s, t)) = \text{image}_2(f', s, g'(t)). \]

Finset.image₂_image_left_comm theorem

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

Full source

/-- Symmetric statement to `Finset.image_image₂_distrib_left`. -/
theorem image₂_image_left_comm {f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ}
    (h_left_comm : ∀ a b, f (g a) b = g' (f' a b)) :
    image₂ f (s.image g) t = (image₂ f' s t).image g' :=
  (image_image₂_distrib_left fun a b => (h_left_comm a b).symm).symm

Left-commutative property of binary image operations on finite sets: $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 finite 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{image}_2(f, g(s), t) = g'(\text{image}_2(f', s, t)). \]

Finset.image_image₂_right_comm theorem

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

Full source

/-- Symmetric statement to `Finset.image_image₂_distrib_right`. -/
theorem image_image₂_right_comm {f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ}
    (h_right_comm : ∀ a b, f a (g b) = g' (f' a b)) :
    image₂ f s (t.image g) = (image₂ f' s t).image g' :=
  (image_image₂_distrib_right fun a b => (h_right_comm a b).symm).symm

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

Informal description

Let $f : \alpha \to \beta' \to \gamma$, $g : \beta \to \beta'$, $f' : \alpha \to \beta \to \delta$, and $g' : \delta \to \gamma$ be functions such that for all $a \in \alpha$ and $b \in \beta$, the right commutative property $f(a, g(b)) = g'(f'(a, b))$ holds. Then for any finite subsets $s \subseteq \alpha$ and $t \subseteq \beta$, we have: \[ \text{image}_2(f, s, g(t)) = g'(\text{image}_2(f', s, t)). \]

Finset.image₂_distrib_subset_left theorem

 {γ : Type*} {u : Finset γ} {f : α → δ → ε} {g : β → γ → δ} {f₁ : α → β → β'} {f₂ : α → γ → γ'} {g' : β' → γ' → ε}
  (h_distrib : ∀ a b c, f a (g b c) = g' (f₁ a b) (f₂ a c)) :
  image₂ f s (image₂ g t u) ⊆ image₂ g' (image₂ f₁ s t) (image₂ f₂ s u)

Full source

/-- The other direction does not hold because of the `s`-`s` cross terms on the RHS. -/
theorem image₂_distrib_subset_left {γ : Type*} {u : Finset γ} {f : α → δ → ε} {g : β → γ → δ}
    {f₁ : α → β → β'} {f₂ : α → γ → γ'} {g' : β' → γ' → ε}
    (h_distrib : ∀ a b c, f a (g b c) = g' (f₁ a b) (f₂ a c)) :
    image₂image₂ f s (image₂ g t u) ⊆ image₂ g' (image₂ f₁ s t) (image₂ f₂ s u) :=
  coe_subset.1 <| by
    push_cast
    exact Set.image2_distrib_subset_left h_distrib

Left Distributivity of Binary Image Operation on Finite Sets

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 finite sets $s \subseteq \alpha$, $t \subseteq \beta$, and $u \subseteq \gamma$, we have the subset relation: \[ \text{image}_2(f, s, \text{image}_2(g, t, u)) \subseteq \text{image}_2(g', \text{image}_2(f_1, s, t), \text{image}_2(f_2, s, u)). \]

Finset.image₂_distrib_subset_right theorem

 {γ : Type*} {u : Finset γ} {f : δ → γ → ε} {g : α → β → δ} {f₁ : α → γ → α'} {f₂ : β → γ → β'} {g' : α' → β' → ε}
  (h_distrib : ∀ a b c, f (g a b) c = g' (f₁ a c) (f₂ b c)) :
  image₂ f (image₂ g s t) u ⊆ image₂ g' (image₂ f₁ s u) (image₂ f₂ t u)

Full source

/-- The other direction does not hold because of the `u`-`u` cross terms on the RHS. -/
theorem image₂_distrib_subset_right {γ : Type*} {u : Finset γ} {f : δ → γ → ε} {g : α → β → δ}
    {f₁ : α → γ → α'} {f₂ : β → γ → β'} {g' : α' → β' → ε}
    (h_distrib : ∀ a b c, f (g a b) c = g' (f₁ a c) (f₂ b c)) :
    image₂image₂ f (image₂ g s t) u ⊆ image₂ g' (image₂ f₁ s u) (image₂ f₂ t u) :=
  coe_subset.1 <| by
    push_cast
    exact Set.image2_distrib_subset_right h_distrib

Right Distributive Property of Binary Image of Finite 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 finite sets $s \subseteq \alpha$, $t \subseteq \beta$, and $u \subseteq \gamma$, we have the inclusion: \[ \text{image}_2(f, \text{image}_2(g, s, t), u) \subseteq \text{image}_2(g', \text{image}_2(f_1, s, u), \text{image}_2(f_2, t, u)). \]

Finset.image_image₂_antidistrib theorem

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

Full source

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

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

Informal description

Let $f \colon \alpha \times \beta \to \gamma$ be a binary function, $g \colon \gamma \to \delta$ a function, and $f' \colon \beta' \times \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 finite subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the binary image $\text{image}_2(f, s, t)$ under $g$ equals the binary image of $g_1(t)$ and $g_2(s)$ under $f'$: \[ g(\text{image}_2(f, s, t)) = \text{image}_2(f', g_1(t), g_2(s)). \]

Finset.image_image₂_antidistrib_left theorem

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

Full source

/-- Symmetric statement to `Finset.image₂_image_left_anticomm`. -/
theorem image_image₂_antidistrib_left {g : γ → δ} {f' : β' → α → δ} {g' : β → β'}
    (h_antidistrib : ∀ a b, g (f a b) = f' (g' b) a) :
    (image₂ f s t).image g = image₂ f' (t.image g') s :=
  coe_injective <| by
    push_cast
    exact image_image2_antidistrib_left h_antidistrib

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

Informal description

Let $f \colon \alpha \times \beta \to \gamma$ be a binary function, $g \colon \gamma \to \delta$ a function, and $f' \colon \beta' \times \alpha \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 antidistributive property $g(f(a, b)) = f'(g'(b), a)$ holds. Then for any finite subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the binary image $\text{image}_2(f, s, t)$ under $g$ equals the binary image of $g'(t)$ and $s$ under $f'$: \[ g(\text{image}_2(f, s, t)) = \text{image}_2(f', g'(t), s). \]

Finset.image_image₂_antidistrib_right theorem

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

Full source

/-- Symmetric statement to `Finset.image_image₂_right_anticomm`. -/
theorem image_image₂_antidistrib_right {g : γ → δ} {f' : β → α' → δ} {g' : α → α'}
    (h_antidistrib : ∀ a b, g (f a b) = f' b (g' a)) :
    (image₂ f s t).image g = image₂ f' t (s.image g') :=
  coe_injective <| by
    push_cast
    exact image_image2_antidistrib_right h_antidistrib

Right Antidistributivity of Image over Binary Image of Finite Sets: $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 finite subsets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the binary image $\text{image}_2(f, s, t)$ under $g$ equals the binary image of $t$ and $g'(s)$ under $f'$: \[ g(\text{image}_2(f, s, t)) = \text{image}_2(f', t, g'(s)). \]

Finset.image₂_image_left_anticomm theorem

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

Full source

/-- Symmetric statement to `Finset.image_image₂_antidistrib_left`. -/
theorem image₂_image_left_anticomm {f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ}
    (h_left_anticomm : ∀ a b, f (g a) b = g' (f' b a)) :
    image₂ f (s.image g) t = (image₂ f' t s).image g' :=
  (image_image₂_antidistrib_left fun a b => (h_left_anticomm b a).symm).symm

Left Anticommutativity of Binary Image Composition: $\text{image}_2(f, g(s), t) = g'(\text{image}_2(f', t, s))$

Informal description

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

Finset.image_image₂_right_anticomm theorem

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

Full source

/-- Symmetric statement to `Finset.image_image₂_antidistrib_right`. -/
theorem image_image₂_right_anticomm {f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ}
    (h_right_anticomm : ∀ a b, f a (g b) = g' (f' b a)) :
    image₂ f s (t.image g) = (image₂ f' t s).image g' :=
  (image_image₂_antidistrib_right fun a b => (h_right_anticomm b a).symm).symm

Right Anticommutativity of Binary Image Composition: $\text{image}_2(f, s, g(t)) = g'(\text{image}_2(f', t, s))$

Informal description

Let $f \colon \alpha \to \beta' \to \gamma$, $g \colon \beta \to \beta'$, $f' \colon \beta \to \alpha \to \delta$, 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 finite 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 $t$ and $s$ under $f'$: \[ \text{image}_2(f, s, g(t)) = g'(\text{image}_2(f', t, s)). \]

Finset.image₂_left_identity theorem

{f : α → γ → γ} {a : α} (h : ∀ b, f a b = b) (t : Finset γ) : image₂ f { a } t = t

Full source

/-- If `a` is a left identity for `f : α → β → β`, then `{a}` is a left identity for
`Finset.image₂ f`. -/
theorem image₂_left_identity {f : α → γ → γ} {a : α} (h : ∀ b, f a b = b) (t : Finset γ) :
    image₂ f {a} t = t :=
  coe_injective <| by rw [coe_image₂, coe_singleton, Set.image2_left_identity h]

Left identity property for binary image of finite sets

Informal description

Let $f : \alpha \to \gamma \to \gamma$ be a binary function and $a \in \alpha$ be such that $f(a, b) = b$ for all $b \in \gamma$. Then for any finite set $t \subseteq \gamma$, the binary image $\text{image}_2(f, \{a\}, t)$ equals $t$.

Finset.image₂_right_identity theorem

{f : γ → β → γ} {b : β} (h : ∀ a, f a b = a) (s : Finset γ) : image₂ f s { b } = s

Full source

/-- If `b` is a right identity for `f : α → β → α`, then `{b}` is a right identity for
`Finset.image₂ f`. -/
theorem image₂_right_identity {f : γ → β → γ} {b : β} (h : ∀ a, f a b = a) (s : Finset γ) :
    image₂ f s {b} = s := by rw [image₂_singleton_right, funext h, image_id']

Right identity property for binary image of finite sets

Informal description

Let $f : \gamma \to \beta \to \gamma$ be a binary function and $b \in \beta$ be such that $f(a, b) = a$ for all $a \in \gamma$. Then for any finite set $s \subseteq \gamma$, the binary image $\text{image}_2(f, s, \{b\})$ equals $s$.

Finset.card_dvd_card_image₂_right theorem

 (hf : ∀ a ∈ s, Injective (f a)) (hs : ((fun a => t.image <| f a) '' s).PairwiseDisjoint id) : #t ∣ #(image₂ f s t)

Full source

/-- If each partial application of `f` is injective, and images of `s` under those partial
applications are disjoint (but not necessarily distinct!), then the size of `t` divides the size of
`Finset.image₂ f s t`. -/
theorem card_dvd_card_image₂_right (hf : ∀ a ∈ s, Injective (f a))
    (hs : ((fun a => t.image <| f a) '' s).PairwiseDisjoint id) : #t#t ∣ #(image₂ f s t) := by
  classical
  induction' s using Finset.induction with a s _ ih
  · simp
  specialize ih (forall_of_forall_insert hf)
    (hs.subset <| Set.image_subset _ <| coe_subset.2 <| subset_insert _ _)
  rw [image₂_insert_left]
  by_cases h : Disjoint (image (f a) t) (image₂ f s t)
  · rw [card_union_of_disjoint h]
    exact Nat.dvd_add (card_image_of_injective _ <| hf _ <| mem_insert_self _ _).symm.dvd ih
  simp_rw [← biUnion_image_left, disjoint_biUnion_right, not_forall] at h
  obtain ⟨b, hb, h⟩ := h
  rwa [union_eq_right.2]
  exact (hs.eq (Set.mem_image_of_mem _ <| mem_insert_self _ _)
      (Set.mem_image_of_mem _ <| mem_insert_of_mem hb) h).trans_subset
    (image_subset_image₂_right hb)

Divisibility of Binary Image Cardinality under Partial Injectivity and Disjointness

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a binary function, $s$ a finite subset of $\alpha$, and $t$ a finite subset of $\beta$. Suppose that for every $a \in s$, the partial function $f(a, \cdot) : \beta \to \gamma$ is injective, and that the images $\{f(a, b) \mid b \in t\}$ for $a \in s$ are pairwise disjoint. Then the cardinality of $t$ divides the cardinality of the binary image $\text{image}_2(f, s, t) = \{f(a, b) \mid a \in s, b \in t\}$.

Finset.card_dvd_card_image₂_left theorem

 (hf : ∀ b ∈ t, Injective fun a => f a b) (ht : ((fun b => s.image fun a => f a b) '' t).PairwiseDisjoint id) :
  #s ∣ #(image₂ f s t)

Full source

/-- If each partial application of `f` is injective, and images of `t` under those partial
applications are disjoint (but not necessarily distinct!), then the size of `s` divides the size of
`Finset.image₂ f s t`. -/
theorem card_dvd_card_image₂_left (hf : ∀ b ∈ t, Injective fun a => f a b)
    (ht : ((fun b => s.image fun a => f a b) '' t).PairwiseDisjoint id) :
    #s#s ∣ #(image₂ f s t) := by rw [← image₂_swap]; exact card_dvd_card_image₂_right hf ht

Divisibility of Binary Image Cardinality under Left Partial Injectivity and Disjointness

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a binary function, $s$ a finite subset of $\alpha$, and $t$ a finite subset of $\beta$. Suppose that for every $b \in t$, the partial function $f(\cdot, b) : \alpha \to \gamma$ is injective, and that the images $\{f(a, b) \mid a \in s\}$ for $b \in t$ are pairwise disjoint. Then the cardinality of $s$ divides the cardinality of the binary image $\text{image}_2(f, s, t) = \{f(a, b) \mid a \in s, b \in t\}$.

Finset.subset_set_image₂ theorem

 {s : Set α} {t : Set β} (hu : ↑u ⊆ image2 f s t) :
  ∃ (s' : Finset α) (t' : Finset β), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t'

Full source

/-- If a `Finset` is a subset of the image of two `Set`s under a binary operation,
then it is a subset of the `Finset.image₂` of two `Finset` subsets of these `Set`s. -/
theorem subset_set_image₂ {s : Set α} {t : Set β} (hu : ↑u ⊆ image2 f s t) :
    ∃ (s' : Finset α) (t' : Finset β), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t' := by
  rw [← Set.image_prod, subset_set_image_iff] at hu
  rcases hu with ⟨u, hu, rfl⟩
  classical
  use u.image Prod.fst, u.image Prod.snd
  simp only [coe_image, Set.image_subset_iff, image₂_image_left, image₂_image_right,
    image_subset_iff]
  exact ⟨fun _ h ↦ (hu h).1, fun _ h ↦ (hu h).2, fun x hx ↦ mem_image₂_of_mem hx hx⟩

Finite subset of binary image is contained in finite binary image of subsets

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a binary function, $s \subseteq \alpha$ and $t \subseteq \beta$ be sets, and $u$ be a finite subset of $\gamma$ such that $u \subseteq \{f(a,b) \mid a \in s, b \in t\}$. Then there exist finite subsets $s' \subseteq s$ and $t' \subseteq t$ such that $u \subseteq \{f(a,b) \mid a \in s', b \in t'\}$.

Finset.image₂_inter_union_subset_union theorem

: image₂ f (s ∩ s') (t ∪ t') ⊆ image₂ f s t ∪ image₂ f s' t'

Full source

theorem image₂_inter_union_subset_union :
    image₂image₂ f (s ∩ s') (t ∪ t') ⊆ image₂ f s t ∪ image₂ f s' t' :=
  coe_subset.1 <| by
    push_cast
    exact Set.image2_inter_union_subset_union

Subset Property for Binary Image on Intersection-Union Pairs of Finite Sets

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and finite 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'\}. \]

Finset.image₂_union_inter_subset_union theorem

: image₂ f (s ∪ s') (t ∩ t') ⊆ image₂ f s t ∪ image₂ f s' t'

Full source

theorem image₂_union_inter_subset_union :
    image₂image₂ f (s ∪ s') (t ∩ t') ⊆ image₂ f s t ∪ image₂ f s' t' :=
  coe_subset.1 <| by
    push_cast
    exact Set.image2_union_inter_subset_union

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

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and finite sets $s, s' \subseteq \alpha$, $t, t' \subseteq \beta$, the binary image of $f$ over the union $s \cup s'$ and the intersection $t \cap t'$ is a subset of the union of the binary images of $f$ over $s \times t$ and $s' \times t'$. In other words, \[ \text{image}_2(f, s \cup s', t \cap t') \subseteq \text{image}_2(f, s, t) \cup \text{image}_2(f, s', t'). \]

Finset.image₂_inter_union_subset theorem

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

Full source

theorem image₂_inter_union_subset {f : α → α → β} {s t : Finset α} (hf : ∀ a b, f a b = f b a) :
    image₂image₂ f (s ∩ t) (s ∪ t) ⊆ image₂ f s t :=
  coe_subset.1 <| by
    push_cast
    exact image2_inter_union_subset hf

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

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 finite 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\}. \]

Finset.image₂_union_inter_subset theorem

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

Full source

theorem image₂_union_inter_subset {f : α → α → β} {s t : Finset α} (hf : ∀ a b, f a b = f b a) :
    image₂image₂ f (s ∪ t) (s ∩ t) ⊆ image₂ f s t :=
  coe_subset.1 <| by
    push_cast
    exact image2_union_inter_subset hf

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

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 finite 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\}. \]

Finset.sup'_image₂_le theorem

 {g : γ → δ} {a : δ} (h : (image₂ f s t).Nonempty) : sup' (image₂ f s t) h g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a

Full source

@[simp (default + 1)] -- otherwise `simp` doesn't use `forall_mem_image₂`
lemma sup'_image₂_le {g : γ → δ} {a : δ} (h : (image₂ f s t).Nonempty) :
    sup'sup' (image₂ f s t) h g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a := by
  rw [sup'_le_iff, forall_mem_image₂]

Supremum Bound Characterization for Binary Image: $\sup' (\mathrm{image}_2(f, s, t)) g \leq a \leftrightarrow \forall x \in s, \forall y \in t, g(f(x, y)) \leq a$

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a binary function, $s$ and $t$ be finite subsets of $\alpha$ and $\beta$ respectively, and $g : \gamma \to \delta$ be a function. Suppose the image $\mathrm{image}_2(f, s, t)$ is nonempty (with proof $h$). Then for any $a \in \delta$, the following are equivalent: 1. The supremum of $g$ over $\mathrm{image}_2(f, s, t)$ is less than or equal to $a$. 2. For all $x \in s$ and $y \in t$, we have $g(f(x, y)) \leq a$.

Finset.sup'_image₂_left theorem

 (g : γ → δ) (h : (image₂ f s t).Nonempty) :
  sup' (image₂ f s t) h g = sup' s h.of_image₂_left fun x ↦ sup' t h.of_image₂_right (g <| f x ·)

Full source

lemma sup'_image₂_left (g : γ → δ) (h : (image₂ f s t).Nonempty) :
    sup' (image₂ f s t) h g =
      sup' s h.of_image₂_left fun x ↦ sup' t h.of_image₂_right (g <| f x ·) := by
  simp only [image₂, sup'_image, sup'_product_left]; rfl

Supremum of Binary Image Equals Iterated Supremum (Left Version)

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a binary function, $s$ and $t$ be finite subsets of $\alpha$ and $\beta$ respectively, and $g : \gamma \to \delta$ be a function where $\delta$ is a join-semilattice. If the binary image $\mathrm{image}_2(f, s, t)$ is nonempty (with proof $h$), then the supremum of $g$ over $\mathrm{image}_2(f, s, t)$ equals the supremum over $s$ of the functions that take each $x \in s$ to the supremum over $t$ of the functions $y \mapsto g(f(x, y))$. In symbols: $$ \sup'_{\mathrm{image}_2(f, s, t)} g = \sup'_{x \in s} \left( \sup'_{y \in t} g(f(x, y)) \right) $$

Finset.sup'_image₂_right theorem

 (g : γ → δ) (h : (image₂ f s t).Nonempty) :
  sup' (image₂ f s t) h g = sup' t h.of_image₂_right fun y ↦ sup' s h.of_image₂_left (g <| f · y)

Full source

lemma sup'_image₂_right (g : γ → δ) (h : (image₂ f s t).Nonempty) :
    sup' (image₂ f s t) h g =
      sup' t h.of_image₂_right fun y ↦ sup' s h.of_image₂_left (g <| f · y) := by
  simp only [image₂, sup'_image, sup'_product_right]; rfl

Supremum of Binary Image Equals Iterated Supremum (Right Version)

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a binary function, $s$ and $t$ be finite subsets of $\alpha$ and $\beta$ respectively, and $g : \gamma \to \delta$ be a function where $\delta$ is a join-semilattice. If the binary image $\mathrm{image}_2(f, s, t)$ is nonempty (with proof $h$), then the supremum of $g$ over $\mathrm{image}_2(f, s, t)$ equals the supremum over $t$ of the functions that take each $y \in t$ to the supremum over $s$ of the functions $x \mapsto g(f(x, y))$. In symbols: $$ \sup'_{\mathrm{image}_2(f, s, t)} g = \sup'_{y \in t} \left( \sup'_{x \in s} g(f(x, y)) \right) $$

Finset.sup_image₂_le theorem

{g : γ → δ} {a : δ} : sup (image₂ f s t) g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a

Full source

@[simp (default + 1)] -- otherwise `simp` doesn't use `forall_mem_image₂`
lemma sup_image₂_le {g : γ → δ} {a : δ} :
    supsup (image₂ f s t) g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a := by
  rw [Finset.sup_le_iff, forall_mem_image₂]

Supremum Bound for Binary Image: $\sup_{z \in \mathrm{image}_2(f,s,t)} g(z) \leq a \leftrightarrow \forall x \in s, \forall y \in t, g(f(x,y)) \leq a$

Informal description

Let $s$ and $t$ be finite sets of types $\alpha$ and $\beta$ respectively, $f : \alpha \to \beta \to \gamma$ a binary function, and $g : \gamma \to \delta$ a function where $\delta$ is a join-semilattice with a bottom element. For any $a \in \delta$, the supremum of $g$ over the binary image $\mathrm{image}_2(f, s, t)$ is less than or equal to $a$ if and only if for all $x \in s$ and $y \in t$, $g(f(x, y)) \leq a$.

Finset.sup_image₂_left theorem

(g : γ → δ) : sup (image₂ f s t) g = sup s fun x ↦ sup t (g <| f x ·)

Full source

lemma sup_image₂_left (g : γ → δ) : sup (image₂ f s t) g = sup s fun x ↦ sup t (g <| f x ·) := by
  simp only [image₂, sup_image, sup_product_left]; rfl

Supremum over Binary Image Equals Iterated Supremum (Left Version)

Informal description

Let $s$ and $t$ be finite sets of types $\alpha$ and $\beta$ respectively, and let $f : \alpha \to \beta \to \gamma$ be a binary function. For any function $g : \gamma \to \delta$ where $\delta$ is a join-semilattice with a bottom element, the supremum of $g$ over the binary image $\text{image}_2(f, s, t)$ is equal to the supremum over $s$ of the functions that take each $x \in s$ to the supremum over $t$ of $g(f(x, y))$. In other words, \[ \sup_{z \in \text{image}_2(f, s, t)} g(z) = \sup_{x \in s} \left( \sup_{y \in t} g(f(x, y)) \right). \]

Finset.sup_image₂_right theorem

(g : γ → δ) : sup (image₂ f s t) g = sup t fun y ↦ sup s (g <| f · y)

Full source

lemma sup_image₂_right (g : γ → δ) : sup (image₂ f s t) g = sup t fun y ↦ sup s (g <| f · y) := by
  simp only [image₂, sup_image, sup_product_right]; rfl

Supremum over Binary Image Equals Iterated Supremum (Right Version)

Informal description

Let $s$ and $t$ be finite sets of types $\alpha$ and $\beta$ respectively, and let $f : \alpha \to \beta \to \gamma$ be a binary function. For any function $g : \gamma \to \delta$ where $\delta$ is a join-semilattice with a bottom element, the supremum of $g$ over the binary image $\text{image}_2(f, s, t)$ is equal to the supremum over $t$ of the functions that take each $y \in t$ to the supremum over $s$ of $g(f(x, y))$. In other words, \[ \sup_{z \in \text{image}_2(f, s, t)} g(z) = \sup_{y \in t} \left( \sup_{x \in s} g(f(x, y)) \right). \]

Finset.le_inf'_image₂ theorem

 {g : γ → δ} {a : δ} (h : (image₂ f s t).Nonempty) : a ≤ inf' (image₂ f s t) h g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)

Full source

@[simp (default + 1)] -- otherwise `simp` doesn't use `forall_mem_image₂`
lemma le_inf'_image₂ {g : γ → δ} {a : δ} (h : (image₂ f s t).Nonempty) :
    a ≤ inf' (image₂ f s t) h g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y) := by
  rw [le_inf'_iff, forall_mem_image₂]

Characterization of Infimum Bound for Binary Image: $a \leq \inf' \text{image}_2(f, s, t) g \leftrightarrow \forall x \in s, \forall y \in t, a \leq g(f(x, y))$

Informal description

Let $s$ and $t$ be finite sets of types $\alpha$ and $\beta$ respectively, $f : \alpha \to \beta \to \gamma$ a binary function, and $g : \gamma \to \delta$ a function where $\delta$ is a meet-semilattice. For any element $a \in \delta$ and nonempty binary image $\text{image}_2(f, s, t)$, the following equivalence holds: \[ a \leq \inf'_{z \in \text{image}_2(f, s, t)} g(z) \leftrightarrow \forall x \in s, \forall y \in t, a \leq g(f(x, y)). \] Here, $\inf'$ denotes the infimum over a nonempty finite set in the meet-semilattice $\delta$.

Finset.inf'_image₂_left theorem

 (g : γ → δ) (h : (image₂ f s t).Nonempty) :
  inf' (image₂ f s t) h g = inf' s h.of_image₂_left fun x ↦ inf' t h.of_image₂_right (g <| f x ·)

Full source

lemma inf'_image₂_left (g : γ → δ) (h : (image₂ f s t).Nonempty) :
    inf' (image₂ f s t) h g =
      inf' s h.of_image₂_left fun x ↦ inf' t h.of_image₂_right (g <| f x ·) :=
  sup'_image₂_left (δ := δᵒᵈ) g h

Iterated Infimum Equality for Binary Image (Left Version)

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a binary function, $s$ and $t$ be finite subsets of $\alpha$ and $\beta$ respectively, and $g : \gamma \to \delta$ be a function where $\delta$ is a meet-semilattice. If the binary image $\mathrm{image}_2(f, s, t)$ is nonempty (with proof $h$), then the infimum of $g$ over $\mathrm{image}_2(f, s, t)$ equals the infimum over $s$ of the functions that take each $x \in s$ to the infimum over $t$ of the functions $y \mapsto g(f(x, y))$. In symbols: $$ \inf'_{\mathrm{image}_2(f, s, t)} g = \inf'_{x \in s} \left( \inf'_{y \in t} g(f(x, y)) \right) $$

Finset.inf'_image₂_right theorem

 (g : γ → δ) (h : (image₂ f s t).Nonempty) :
  inf' (image₂ f s t) h g = inf' t h.of_image₂_right fun y ↦ inf' s h.of_image₂_left (g <| f · y)

Full source

lemma inf'_image₂_right (g : γ → δ) (h : (image₂ f s t).Nonempty) :
    inf' (image₂ f s t) h g =
      inf' t h.of_image₂_right fun y ↦ inf' s h.of_image₂_left (g <| f · y) :=
  sup'_image₂_right (δ := δᵒᵈ) g h

Infimum of Binary Image Equals Iterated Infimum (Right Version)

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a binary function, $s \subseteq \alpha$ and $t \subseteq \beta$ be finite sets, and $g : \gamma \to \delta$ be a function where $\delta$ is a meet-semilattice. If the binary image $\mathrm{image}_2(f, s, t)$ is nonempty (with proof $h$), then the infimum of $g$ over $\mathrm{image}_2(f, s, t)$ equals the infimum over $t$ of the functions that take each $y \in t$ to the infimum over $s$ of the functions $x \mapsto g(f(x, y))$. In symbols: \[ \inf'_{\mathrm{image}_2(f, s, t)} g = \inf'_{y \in t} \left( \inf'_{x \in s} g(f(x, y)) \right) \]

Finset.le_inf_image₂ theorem

{g : γ → δ} {a : δ} : a ≤ inf (image₂ f s t) g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)

Full source

@[simp (default + 1)] -- otherwise `simp` doesn't use `forall_mem_image₂`
lemma le_inf_image₂ {g : γ → δ} {a : δ} :
    a ≤ inf (image₂ f s t) g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y) :=
  sup_image₂_le (δ := δᵒᵈ)

Infimum Bound for Binary Image: $a \leq \inf_{z \in \mathrm{image}_2(f,s,t)} g(z) \leftrightarrow \forall x \in s, \forall y \in t, a \leq g(f(x,y))$

Informal description

Let $s$ and $t$ be finite sets of types $\alpha$ and $\beta$ respectively, $f : \alpha \to \beta \to \gamma$ a binary function, and $g : \gamma \to \delta$ a function where $\delta$ is a meet-semilattice with a top element. For any $a \in \delta$, we have $a \leq \inf_{z \in \mathrm{image}_2(f,s,t)} g(z)$ if and only if for all $x \in s$ and $y \in t$, $a \leq g(f(x,y))$.

Finset.inf_image₂_left theorem

(g : γ → δ) : inf (image₂ f s t) g = inf s fun x ↦ inf t (g ∘ f x)

Full source

lemma inf_image₂_left (g : γ → δ) : inf (image₂ f s t) g = inf s fun x ↦ inf t (g ∘ f x) :=
  sup_image₂_left (δ := δᵒᵈ) ..

Infimum over Binary Image Equals Iterated Infimum (Left Version)

Informal description

Let $s$ and $t$ be finite sets of types $\alpha$ and $\beta$ respectively, and let $f : \alpha \to \beta \to \gamma$ be a binary function. For any function $g : \gamma \to \delta$ where $\delta$ is a meet-semilattice with a top element, the infimum of $g$ over the binary image $\text{image}_2(f, s, t)$ is equal to the infimum over $s$ of the functions that take each $x \in s$ to the infimum over $t$ of $g(f(x, y))$. In other words, \[ \inf_{z \in \text{image}_2(f, s, t)} g(z) = \inf_{x \in s} \left( \inf_{y \in t} g(f(x, y)) \right). \]

Finset.inf_image₂_right theorem

(g : γ → δ) : inf (image₂ f s t) g = inf t fun y ↦ inf s (g <| f · y)

Full source

lemma inf_image₂_right (g : γ → δ) : inf (image₂ f s t) g = inf t fun y ↦ inf s (g <| f · y) :=
  sup_image₂_right (δ := δᵒᵈ) ..

Infimum over Binary Image Equals Iterated Infimum (Right Version)

Informal description

Let $s$ and $t$ be finite sets of types $\alpha$ and $\beta$ respectively, and let $f : \alpha \to \beta \to \gamma$ be a binary function. For any function $g : \gamma \to \delta$ where $\delta$ is a meet-semilattice with a top element, the infimum of $g$ over the binary image $\text{image}_2(f, s, t)$ is equal to the infimum over $t$ of the functions that take each $y \in t$ to the infimum over $s$ of $g(f(x, y))$. In other words, \[ \inf_{z \in \text{image}_2(f, s, t)} g(z) = \inf_{y \in t} \left( \inf_{x \in s} g(f(x, y)) \right). \]

Fintype.piFinset_image₂ theorem

 (f : ∀ i, α i → β i → γ i) (s : ∀ i, Finset (α i)) (t : ∀ i, Finset (β i)) :
  piFinset (fun i ↦ image₂ (f i) (s i) (t i)) = image₂ (fun a b i ↦ f _ (a i) (b i)) (piFinset s) (piFinset t)

Full source

lemma piFinset_image₂ (f : ∀ i, α i → β i → γ i) (s : ∀ i, Finset (α i)) (t : ∀ i, Finset (β i)) :
    piFinset (fun i ↦ image₂ (f i) (s i) (t i)) =
      image₂ (fun a b i ↦ f _ (a i) (b i)) (piFinset s) (piFinset t) := by
  ext; simp only [mem_piFinset, mem_image₂, Classical.skolem, forall_and, funext_iff]

Compatibility of Finite Product with Binary Image: $\prod_i \text{image}_2(f_i, s_i, t_i) = \text{image}_2(\lambda a b i, f_i (a i) (b i), \prod_i s_i, \prod_i t_i)$

Informal description

For a family of binary functions $f_i : \alpha_i \to \beta_i \to \gamma_i$ indexed by $i$, and families of finite sets $s_i \subseteq \alpha_i$ and $t_i \subseteq \beta_i$, the finite product of the binary images $\prod_i \text{image}_2(f_i, s_i, t_i)$ is equal to the binary image of the finite products $\text{image}_2(\lambda a b i, f_i (a i) (b i), \prod_i s_i, \prod_i t_i)$. In other words, the following diagram commutes: $$\prod_i \text{image}_2(f_i, s_i, t_i) = \text{image}_2\left((a,b) \mapsto (i \mapsto f_i(a_i, b_i)), \prod_i s_i, \prod_i t_i\right)$$

Set.toFinset_image2 theorem

 (f : α → β → γ) (s : Set α) (t : Set β) [Fintype s] [Fintype t] [Fintype (image2 f s t)] :
  (image2 f s t).toFinset = Finset.image₂ f s.toFinset t.toFinset

Full source

@[simp]
theorem toFinset_image2 (f : α → β → γ) (s : Set α) (t : Set β) [Fintype s] [Fintype t]
    [Fintype (image2 f s t)] : (image2 f s t).toFinset = Finset.image₂ f s.toFinset t.toFinset :=
  Finset.coe_injective <| by simp

Equality of Binary Image Conversions: $\text{image2}(f, s, t).\text{toFinset} = \text{image}_2(f, s.\text{toFinset}, t.\text{toFinset})$

Informal description

For any binary function $f : \alpha \to \beta \to \gamma$ and finite sets $s \subseteq \alpha$, $t \subseteq \beta$ (with `Fintype` instances for $s$, $t$, and $\text{image2}(f, s, t)$), the finite set obtained by converting the image set $\text{image2}(f, s, t)$ to a `Finset` is equal to the binary image $\text{image}_2(f, s.\text{toFinset}, t.\text{toFinset})$ of the finite sets $s.\text{toFinset}$ and $t.\text{toFinset}$ under $f$.

Notes