Finset.mem_image₂_of_mem
theorem Finset.mem_image₂_of_mem :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
{a : α} {b : β}, a ∈ s → b ∈ t → f a b ∈ Finset.image₂ f s t
The theorem `Finset.mem_image₂_of_mem` states that for any types `α`, `β`, and `γ` where `γ` has decidable equality, given a binary function `f : α → β → γ`, two finite sets `s : Finset α` and `t : Finset β`, and elements `a : α` and `b : β`, if `a` is an element of `s` and `b` is an element of `t`, then the application of the function `f` to `a` and `b` (i.e., `f a b`) is an element of the image of the function `f` applied to `s` and `t` (i.e., `f a b` is in the set `Finset.image₂ f s t`). In other words, this theorem asserts that the result of applying a function to elements of two sets belongs to the image of the function on these sets.
More concisely: For functions between finite sets with decidable equality, if an element of the first set is in the first set and an element of the second set is in the second set, then the application of the function to those elements is in the image of the function applied to the two sets.
|
Finset.inf_image₂_left
theorem Finset.inf_image₂_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} (s : Finset α)
(t : Finset β) [inst_1 : SemilatticeInf δ] [inst_2 : OrderTop δ] (g : γ → δ),
(Finset.image₂ f s t).inf g = s.inf fun x => t.inf (g ∘ f x)
This theorem states that for any two finite sets `s` and `t` of types `α` and `β`, respectively, and a binary function `f : α → β → γ`, the infimum of the image of the function `f` over the Cartesian product of `s` and `t`, when transformed by another function `g : γ → δ`, is equal to the infimum of the set `s` transformed by the function which maps each element `x` of `s` to the infimum of the set `t` transformed by the composition of `g` and `f` evaluated at `x`. This holds in the context where `γ` has a decidable equality, and `δ` is a type forming a semilattice with a top element.
More concisely: Given finite sets `s` and `t` of types `α` and `β`, and a binary function `f : α → β → γ` with `γ` being a decidably equated semilattice with top element, the infimum of `g ∘ f(s × t)` equals the infimum of `map (inf inf t) s`.
|
Finset.card_image₂_singleton_right
theorem Finset.card_image₂_singleton_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} (s : Finset α) {b : β},
(Function.Injective fun a => f a b) → (Finset.image₂ f s {b}).card = s.card
The theorem `Finset.card_image₂_singleton_right` states that for any types `α`, `β`, and `γ`, given a binary function `f : α → β → γ` and a finite set `s : Finset α`, if `f` is injective when its second argument is a particular element `b : β`, then the cardinality of the image of `f` applied to `s` and the singleton set `{b}` is equal to the cardinality of `s`. In simpler terms, if applying `f` to each element in `s` and a fixed `b` produces unique results, then the number of such unique results is the same as the number of elements in `s`.
More concisely: If `f : α -> β -> γ` is a function, `s : Finset α`, and `b : β` are such that `f` is injective on `{a : α | exists b', f a b = b}`, then `#(map (lambda x, f x b) s) = #s`.
|
Finset.image_image₂_right_comm
theorem Finset.image_image₂_right_comm :
∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq β']
[inst_1 : DecidableEq γ] [inst_2 : DecidableEq δ] {s : Finset α} {t : Finset β} {f : α → β' → γ} {g : β → β'}
{f' : α → β → δ} {g' : δ → γ},
(∀ (a : α) (b : β), f a (g b) = g' (f' a b)) →
Finset.image₂ f s (Finset.image g t) = Finset.image g' (Finset.image₂ f' s t)
The theorem `Finset.image_image₂_right_comm` states that, for any sets `s` of type `α` and `t` of type `β`, and any functions `f : α → β' → γ`, `g : β → β'`, `f' : α → β → δ`, and `g' : δ → γ`, if for all `a` in `α` and `b` in `β`, `f a (g b)` equals `g' (f' a b)`, then the image under `f` of the Cartesian product of `s` and the image under `g` of `t` equals the image under `g'` of the image under `f'` of the Cartesian product of `s` and `t`. This is a commutation relation between the operations of taking images under certain functions, and it generalizes in a certain sense the property that the image of the union of two sets under a function is the union of the images of the sets.
More concisely: If for all `a` in `α` and `b` in `β`, `f a (g b) = g' (f' a b)`, then `f''(s × t) = g''(f'(s × t))`, where `f'' : α × β → γ`, `g'' : β × α → γ`, `s : set α`, `t : set β`, `f' : α × β → δ`, `g' : δ → γ`, and `f''(x, y) = f x (g y)`, `g''(x, y) = g' (f' x y)`.
|
Finset.image₂_empty_left
theorem Finset.image₂_empty_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {t : Finset β},
Finset.image₂ f ∅ t = ∅
This theorem states that for any types `α`, `β`, and `γ` with `γ` having a decidable equality relation, any binary function `f` from `α` and `β` to `γ`, and any finite set `t` of type `β`, the image of the function `f` when applied to an empty set of type `α` and the set `t` is always an empty set of type `γ`. In mathematical terms, if we consider the function `f : α × β → γ`, the image of the empty set in `α` under this function is always the empty set in `γ`.
More concisely: For any decidably equal types `α`, `β`, and `γ`, and any decidable binary function `f : α × β → γ`, the image of the empty set of `α` under `f` is the empty set of `γ`.
|
Finset.image₂_image_left_anticomm
theorem Finset.image₂_image_left_anticomm :
∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq α']
[inst_1 : DecidableEq γ] [inst_2 : DecidableEq δ] {s : Finset α} {t : Finset β} {f : α' → β → γ} {g : α → α'}
{f' : β → α → δ} {g' : δ → γ},
(∀ (a : α) (b : β), f (g a) b = g' (f' b a)) →
Finset.image₂ f (Finset.image g s) t = Finset.image g' (Finset.image₂ f' t s)
The theorem `Finset.image₂_image_left_anticomm` states that for any types `α`, `α'`, `β`, `γ`, and `δ` with decidable equality on `α'`, `γ`, and `δ`, and any finite sets `s` of type `α` and `t` of type `β`, functions `f : α' → β → γ`, `g : α → α'`, `f' : β → α → δ`, and `g' : δ → γ`, if for all elements `a` of `α` and `b` of `β`, the value of `f` at `g a` and `b` equals to the value of `g'` at `f' b a`, then the image under `f` of the image under `g` of `s` and `t` equals the image under `g'` of the image under `f'` of `t` and `s`. Here, `Finset.image` refers to the forward image of a set under a function, and `Finset.image₂` refers to the image of a binary function on two sets, thought of as the image of the corresponding function on the Cartesian product of the two sets.
More concisely: If `f(ga(s)) = g' (f' b(s, t))` for all `a(s) in s` and `b(t) in t` implies `image₂ f g (s, t) = image₂ g' f' (t, s)`, then the image of the finite sets `s` and `t` under the functions `g` and `f` is equal to the image of the sets `t` and `s` under the functions `f'` and `g'`, respectively.
|
Finset.image₂_empty_right
theorem Finset.image₂_empty_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α},
Finset.image₂ f s ∅ = ∅
The theorem `Finset.image₂_empty_right` states that for all types `α`, `β`, and `γ` such that `γ` has decidable equality, and for any binary function `f` from `α` and `β` to `γ` and any finite set `s` of type `α`, the image of the binary function `f` applied to the finite set `s` and an empty set of type `β` is an empty set. In mathematical terms, given a function $f: \alpha \times \beta \rightarrow \gamma$ and a finite set $s \subseteq \alpha$, if we take the image of $f$ over the Cartesian product of $s$ with an empty set, we get an empty set.
More concisely: For any function $f: \alpha \times \beta \rightarrow \gamma$ with decidable equality on $\gamma$, and any finite set $s \subseteq \alpha$, the image of $f$ applied to the Cartesian product of $s$ and the empty set of $\beta$ is the empty set of $\gamma$.
|
Finset.image₂_singleton_right
theorem Finset.image₂_singleton_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {b : β},
Finset.image₂ f s {b} = Finset.image (fun a => f a b) s
This theorem, `Finset.image₂_singleton_right`, states that for any types `α, β, γ`, where `γ` has decidable equality, for any binary function `f : α → β → γ`, any finite set `s : Finset α`, and any element `b : β`, the image under `f` of the Cartesian product of the set `s` and the singleton set containing `b` is equal to the image under `f` of `s` where `f` is partially applied with `b`. In mathematical terms, this can be expressed as \(f(s \times \{b\}) = \{f(a, b) | a \in s\}\).
More concisely: For any type `γ` with decidable equality, given a binary function `f : α → β → γ` and a finite set `s : Finset α`, the image of the Cartesian product `s × {b}`, for some `b : β`, under `f` is equal to the image of `s` under the partial application of `f` with `b`. In other words, `f(s × {b}) = {f(a, b) | a ∈ s}`.
|
Finset.image₂_union_left
theorem Finset.image₂_union_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s s' : Finset α}
{t : Finset β} [inst_1 : DecidableEq α],
Finset.image₂ f (s ∪ s') t = Finset.image₂ f s t ∪ Finset.image₂ f s' t
The theorem `Finset.image₂_union_left` states that for any types `α`, `β`, `γ`, a binary function `f : α → β → γ`, two finite sets `s` and `s'` of type `α`, and a finite set `t` of type `β`, the image of the function `f` over the union of `s` and `s'` and `t` is equal to the union of the image of `f` over `s` and `t` and the image of `f` over `s'` and `t`. Here, the image of a function over a finite set is defined as the set of all possible outputs of the function when applied to elements in the set. This theorem essentially reflects the distributive property of union over function application.
More concisely: For functions `f : α → β → γ`, sets `s : Finset α`, `s' : Finset α`, and `t : Finset β`, the image of `f` over the union of `s` and `t` is equal to the union of the images of `f` over `s` and `t` and over `s'` and `t`.
|
Finset.image_image₂_distrib_left
theorem Finset.image_image₂_distrib_left :
∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq α']
[inst_1 : DecidableEq γ] [inst_2 : DecidableEq δ] {f : α → β → γ} {s : Finset α} {t : Finset β} {g : γ → δ}
{f' : α' → β → δ} {g' : α → α'},
(∀ (a : α) (b : β), g (f a b) = f' (g' a) b) →
Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' (Finset.image g' s) t
The theorem `Finset.image_image₂_distrib_left` asserts that for any types `α`, `α'`, `β`, `γ`, and `δ` and any functions `f : α → β → γ`, `g : γ → δ`, `f' : α' → β → δ`, and `g' : α → α'`, if for all `a` in `α` and `b` in `β`, the equality `g (f a b) = f' (g' a) b` holds, then taking the image of a binary function `f` on finsets `s` and `t` and then applying `g` is the same as first applying `g'` to `s` and then taking the image of `f'` on the resulting finset and `t`. In other words, the theorem states that image operations commute with each other under certain conditions.
More concisely: Given functions `f : α → β → γ`, `g : γ → δ`, `f' : α' → β → δ`, and `g' : α → α'`, if for all `a` in `α` and `b` in `β`, `g (f a b) = f' (g' a) b`, then `(g ∘ f) (s × t) = g' `^` s × f' `^` t`, where `s` and `t` are finsets and `^` denotes image operation.
|
Finset.image₂_subset_left
theorem Finset.image₂_subset_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α}
{t t' : Finset β}, t ⊆ t' → Finset.image₂ f s t ⊆ Finset.image₂ f s t'
The theorem `Finset.image₂_subset_left` states that for all types `α`, `β`, and `γ` where `γ` has decidable equality, and for all binary functions `f` from `α` and `β` to `γ`, and for any finite sets `s` of `α` and `t` and `t'` of `β`, if set `t` is a subset of set `t'`, then the image of the function `f` applied to `s` and `t` is also a subset of the image of the function `f` applied to `s` and `t'`. In mathematical terms, if $t \subseteq t'$, then $f(s, t) \subseteq f(s, t')$.
More concisely: For all types `α`, `β`, and `γ` with decidable equality, and for all functions `f` from `α × β` to `γ`, if `t ∈ Finset β` is a subset of `t' ∈ Finset β`, then `f''(s, t) ⊆ f''(s, t')` for any `s ∈ Finset α`, where `f''(s, t) := ⋃ i in t, f(s, i)` and `f''(s, t') := ⋃ i in t', f(s, i)`.
|
Finset.image₂_inter_union_subset_union
theorem Finset.image₂_inter_union_subset_union :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s s' : Finset α}
{t t' : Finset β} [inst_1 : DecidableEq α] [inst_2 : DecidableEq β],
Finset.image₂ f (s ∩ s') (t ∪ t') ⊆ Finset.image₂ f s t ∪ Finset.image₂ f s' t'
This theorem states that for any types `α`, `β`, `γ` with `γ` having decidable equality and any binary function `f` from `α` and `β` to `γ`, the image of the function `f` applied to the intersection of two sets `s` and `s'` of `α` and the union of two sets `t` and `t'` of `β` is a subset of the union of the image of `f` applied to `s` and `t` and the image of `f` applied to `s'` and `t'`. This is basically a statement about the behavior of images under intersection and union in the context of binary functions and finite sets.
More concisely: For any types `α`, `β`, `γ` with `γ` having decidable equality, and sets `s ⊆ α`, `s' ⊆ α`, `t ⊆ β`, `t' ⊆ β`, and binary function `f : α × β → γ`, `f`( `s` ∩ `s'`) ⊆ `f`( `s` ∪ `t`) ∪ `f`( `s'` ∪ `t'`) holds.
|
Finset.Nonempty.image₂
theorem Finset.Nonempty.image₂ :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
s.Nonempty → t.Nonempty → (Finset.image₂ f s t).Nonempty
This theorem states that for any types `α`, `β`, and `γ` with decidable equality on `γ`, and any binary function `f` from `α` and `β` to `γ`, if the finsets `s` and `t` (of types `α` and `β` respectively) are nonempty, then the image of the binary function `f` applied to `s` and `t` (i.e., `Finset.image₂ f s t`) is also nonempty. This essentially means that if we have nonempty sets of `α` and `β`, and a function that can combine elements of `α` and `β` to produce elements of `γ`, we are guaranteed to also have a nonempty set of `γ` as a result.
More concisely: For decidably equated types `α`, `β`, and `γ`, if `f` is a binary function from `α × β` to `γ` and `s` and `t` are nonempty finsets of `α` and `β` respectively, then `Finset.image₂ f s t` is nonempty.
|
Finset.image₂_right_identity
theorem Finset.image₂_right_identity :
∀ {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : γ → β → γ} {b : β},
(∀ (a : γ), f a b = a) → ∀ (s : Finset γ), Finset.image₂ f s {b} = s
This theorem asserts that if we have a binary function `f` from types `γ` and `β` to `γ` such that `b` (an element of type `β`) is a right identity for `f` (i.e., for any element `a` of type `γ`, `f(a, b)` equals `a`), then the singleton set `{b}` acts as a right identity for the function `Finset.image₂ f`. Concretely, for any finite set `s` of elements of type `γ`, the image of `s` and `{b}` under `Finset.image₂ f` is equal to `s` itself.
More concisely: If `f` is a binary function from types `γ` and `β` to `γ` such that for any `a : γ`, `f(a, b) = a` for some `b : β`, then for any finite set `s : Finset γ`, `Finset.image₂ f s = s`.
|
Fintype.piFinset_image₂
theorem Fintype.piFinset_image₂ :
∀ {ι : Type u_14} {α : ι → Type u_15} {β : ι → Type u_16} {γ : ι → Type u_17} [inst : DecidableEq ι]
[inst_1 : Fintype ι] [inst_2 : (i : ι) → DecidableEq (γ i)] (f : (i : ι) → α i → β i → γ i)
(s : (i : ι) → Finset (α i)) (t : (i : ι) → Finset (β i)),
(Fintype.piFinset fun i => Finset.image₂ (f i) (s i) (t i)) =
Finset.image₂ (fun a b i => f i (a i) (b i)) (Fintype.piFinset s) (Fintype.piFinset t)
This theorem states that for any types `ι`, `α`, `β`, and `γ` (all indexed by `ι`), given decidable equality on `ι` and on each `γ i`, and the finiteness of `ι`, a function `f` that maps elements of `α i` and `β i` to `γ i`, and two finsets `s` and `t` (indexed by `ι`) of `α i` and `β i` respectively, the image of the binary function `f i` over the cartesian product of `s i` and `t i` for all `i` in `ι` (obtained via `Fintype.piFinset`) is the same as the image of a function that takes a pair of functions `a` and `b` (which are `i` indexed elements of `α i` and `β i` respectively) and an index `i` and applies `f i` to `a i` and `b i`, over the cartesian product of `Fintype.piFinset s` and `Fintype.piFinset t`. In simpler terms, it establishes the equality of two ways of applying a binary function over pairs of elements from finsets, either individually for each index or collectively for all indices.
More concisely: For any types `ι`, `α`, `β`, and `γ`, given decidable equality on `ι` and each `γ ι`, the image of a binary function `f` on the cartesian product of two finsets `s` and `t` (indexed by `ι`) of `α ι` and `β ι`, respectively, is equal to the image of a function that applies `f ι` to pairs of elements from `α ι` and `β ι` over the cartesian product of `s` and `t`.
|
Finset.image_image₂_antidistrib_right
theorem Finset.image_image₂_antidistrib_right :
∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq α']
[inst_1 : DecidableEq γ] [inst_2 : DecidableEq δ] {f : α → β → γ} {s : Finset α} {t : Finset β} {g : γ → δ}
{f' : β → α' → δ} {g' : α → α'},
(∀ (a : α) (b : β), g (f a b) = f' b (g' a)) →
Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' t (Finset.image g' s)
The theorem `Finset.image_image₂_antidistrib_right` asserts that for any sets `s` of type `α` and `t` of type `β`, any functions `f : α → β → γ`, `g : γ → δ`, `f' : β → α' → δ`, and `g' : α → α'`, if for all elements `a` of type `α` and `b` of type `β`, `g (f a b)` equals `f' b (g' a)`, then the image of `g` applied to the image of the binary function `f` on the sets `s` and `t` is equal to the image of the binary function `f'` on the set `t` and the image of `g'` on the set `s`. In mathematical notation, if $g(f(a, b)) = f'(b, g'(a))$ for all $a \in \alpha$ and $b \in \beta$, then $g(Image(f, s, t)) = Image(f', t, g'(s))$.
More concisely: If for all `a` in `α` and `b` in `β`, `g (f a b) = f' b (g' a)`, then `g (Image f s t) = Image f' t (g' s)`.
|
Finset.image₂_inter_subset_right
theorem Finset.image₂_inter_subset_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α}
{t t' : Finset β} [inst_1 : DecidableEq β],
Finset.image₂ f s (t ∩ t') ⊆ Finset.image₂ f s t ∩ Finset.image₂ f s t'
The theorem `Finset.image₂_inter_subset_right` states that for any types `α`, `β`, and `γ`, and for any binary function `f` from `α` and `β` to `γ`, if we have a set `s` of `α` and two sets `t` and `t'` of `β`, then the image of the function `f` over the set `s` and the intersection of `t` and `t'` is a subset of the intersection of the images of the function `f` over `s` and `t`, and over `s` and `t'` respectively. Here, `DecidableEq γ` and `DecidableEq β` denote that equality is decidable for the types `γ` and `β`.
In mathematical notation, it's saying that $f(s, t \cap t') \subseteq f(s, t) \cap f(s, t')$.
More concisely: For any types `α`, `β`, and `γ` with decidable equality, and for any binary function `f` from `α` and `β` to `γ`, if `s` is a set of `α` and `t` and `t'` are sets of `β`, then `f(s, t ∩ t') ⊆ f(s, t) ∩ f(s, t')`.
|
Finset.sup_image₂_le
theorem Finset.sup_image₂_le :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α}
{t : Finset β} [inst_1 : SemilatticeSup δ] [inst_2 : OrderBot δ] {g : γ → δ} {a : δ},
(Finset.image₂ f s t).sup g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a
This theorem states that for any sets `s` of type `α` and `t` of type `β`, a binary function `f` from `α` and `β` to `γ`, a function `g` from `γ` to `δ`, and an element `a` of type `δ` (where `δ` has a join-semilattice structure with a least element), the supremum of the images of the elements of the Cartesian product of `s` and `t` under `f` and then `g` is less than or equal to `a` if and only if for every element `x` in `s` and every element `y` in `t`, the image of `f(x, y)` under `g` is less than or equal to `a`.
More concisely: For sets `s` of type `α`, `t` of type `β`, functions `f : α × β → γ` and `g : γ → δ` (where `δ` is a join-semilattice with least element), and any `a : δ`, the following are equivalent: the supremum of `g ∘ f` over the Cartesian product `s × t` is less than or equal to `a`, and for all `x : α` in `s` and `y : β` in `t`, `g (f x y)` is less than or equal to `a`.
|
Finset.image_subset_image₂_right
theorem Finset.image_subset_image₂_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
{a : α}, a ∈ s → Finset.image (fun b => f a b) t ⊆ Finset.image₂ f s t
The theorem `Finset.image_subset_image₂_right` states that for all types `α`, `β`, `γ`, given a function `f : α → β → γ`, two finite sets `s : Finset α`, `t : Finset β`, and an element `a : α` in `s`, the image of the function `f` when applied to `a` and all elements of `t` is a subset of the image of the function `f` applied to all possible pairings of elements from `s` and `t`. In other words, if we map each element of `t` to `γ` using the function `f` with a fixed `a` from `s`, all these mapped elements are also in the set obtained by considering all possible pairs `(a', b')` where `a'` is from `s` and `b'` is from `t` and mapping these pairs to `γ` using `f`. This theorem is in the context where equality in `γ` is decidable.
More concisely: For all types `α`, `β`, `γ`, function `f : α → β → γ`, finite sets `s : Finset α`, `t : Finset β`, and `a : α` in `s`, the image of `f` applied to `a` and all elements of `t` is a subset of the image of `f` applied to all pairs `(a', b')` with `a'` in `s` and `b'` in `t`.
|
Finset.image₂_union_inter_subset_union
theorem Finset.image₂_union_inter_subset_union :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s s' : Finset α}
{t t' : Finset β} [inst_1 : DecidableEq α] [inst_2 : DecidableEq β],
Finset.image₂ f (s ∪ s') (t ∩ t') ⊆ Finset.image₂ f s t ∪ Finset.image₂ f s' t'
The theorem `Finset.image₂_union_inter_subset_union` states that for any types `α`, `β`, `γ`, a function `f` from `α` to `β` to `γ`, and four arbitrary finite sets `s`, `s'`, `t`, and `t'` of types `α` and `β` respectively with decidable equality on `α`, `β`, and `γ`, the image under `f` of the union of `s` and `s'` and the intersection of `t` and `t'` is a subset of the union of the images under `f` of `s` with `t` and `s'` with `t'`. In mathematical terms, if we treat `f` as a function `f: α × β → γ`, then this theorem says that
```math
f[(s ∪ s') × (t ∩ t')] ⊆ f[s × t] ∪ f[s' × t']
```
More concisely: For any functions `f: α -> β -> γ` and finite sets `s, s', t, t'` of types `α` and `β` with decidable equality, `f(s union s' intersect t intersect t')` is a subset of `f(s intersect t) union f(s intersect t') union f(s' intersect t) union f(s' intersect t')`.
|
Finset.le_inf_image₂
theorem Finset.le_inf_image₂ :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α}
{t : Finset β} [inst_1 : SemilatticeInf δ] [inst_2 : OrderTop δ] {g : γ → δ} {a : δ},
a ≤ (Finset.image₂ f s t).inf g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)
The theorem `Finset.le_inf_image₂` states that for every types `α`, `β`, `γ` and `δ`, with `γ` having a decidable equality, a binary function `f` mapping `α` and `β` to `γ`, two finite sets `s` and `t` of types `α` and `β` respectively, a `SemilatticeInf δ` and `OrderTop δ` instance, a function `g` mapping `γ` to `δ`, and a value `a` of type `δ`, the condition that `a` is less than or equal to the infimum of the image set of `f` applied to `s` and `t` and then mapped through `g`, is equivalent to the condition that for every `x` in `s` and every `y` in `t`, `a` is less than or equal to `g` applied to `f` of `x` and `y`. Here, the infimum is the greatest lower bound of a set.
More concisely: For types `α`, `β`, `γ`, and `δ` with decidable equality, a binary function `f` from `α` to `β`, finite sets `s` of type `α` and `t` of type `β`, a semilattice and ordered topology instance for `δ`, a function `g` from `γ` to `δ`, and a value `a` of type `δ`, the condition that `a <= inf (g . f "" s) ++ g . f "" t` holds if and only if for all `x in s` and `y in t`, `a <= g (f x y)`.
|
Finset.image₂_assoc
theorem Finset.image₂_assoc :
∀ {α : Type u_1} {β : Type u_3} {δ : Type u_7} {ε : Type u_9} {ε' : Type u_10} [inst : DecidableEq δ]
[inst_1 : DecidableEq ε] [inst_2 : DecidableEq ε'] {s : Finset α} {t : Finset β} {γ : Type u_14} {u : Finset γ}
{f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'},
(∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)) →
Finset.image₂ f (Finset.image₂ g s t) u = Finset.image₂ f' s (Finset.image₂ g' t u)
This theorem asserts that for all types `α`, `β`, `δ`, `ε`, `ε'`, `γ`, given decidable equalities on `δ`, `ε`, and `ε'`, and given finsets `s` of type `α`, `t` of type `β`, and `u` of type `γ`, if we have binary functions `f : δ → γ → ε`, `g : α → β → δ`, `f' : α → ε' → ε`, and `g' : β → γ → ε'`, such that for all `a` in `α`, `b` in `β`, and `c` in `γ`, `f (g a b) c` is equal to `f' a (g' b c)`, then the image under `f` of the image under `g` of the cartesian product of `s` and `t`, and `u`, is equal to the image under `f'` of the cartesian product of `s` and the image under `g'` of the cartesian product of `t` and `u`. It is a kind of associativity property for the image of binary functions over finsets.
More concisely: Given decidable equalities on `δ`, `ε`, and `ε'`, and binary functions `f`, `g`, `f'`, `g'`, if `f (g a b) c = f' a (g' b c)` for all `a` in `α`, `b` in `β`, and `c` in `γ`, then `f''(s ×_β t) u = f'(s ×_α t ×_β u)`, where `f'' = λ (s : Set α) (t : Set β) (u : Set γ), ⨄(f'' s t u) := ⨄(⨄(f s t) u)`, and `×_β` denotes the product of sets indexed by `β`.
|
Finset.sup_image₂_right
theorem Finset.sup_image₂_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} (s : Finset α)
(t : Finset β) [inst_1 : SemilatticeSup δ] [inst_2 : OrderBot δ] (g : γ → δ),
(Finset.image₂ f s t).sup g = t.sup fun y => s.sup fun x => g (f x y)
This theorem, `Finset.sup_image₂_right`, states that for any types α, β, γ, δ, a function `f : α → β → γ`, and a function `g : γ → δ`, assuming that `γ` has decidable equality and `δ` forms a semilattice with a bottom element, the supremum of the image of applying `f` to each pair of elements in finsets `s` and `t` and then applying `g` to the result, is the same as the supremum of applying `g ∘ f` to each pair of elements in `s` and `t`, where the supremum is taken first over all elements in `s` and then over all elements in `t`. That is, for each element `y` in `t`, we compute the supremum over all `x` in `s` of `g (f x y)`, and then we take the supremum of the results over all `y` in `t`. This illustrates a form of distributivity of supremum over the image of a binary function.
More concisely: For functions `f : α → β → γ` and `g : γ → δ` between types, given that `γ` has decidable equality and `δ` is a semilattice with a bottom element, the supremum of `g ∘ f` applied to pairs of elements from finsets `s` and `t` is equal to the supremum of `g` applied to the images of each pair under `f`, taken over all pairs in `s` and then over all pairs in `t`.
|
Finset.Nonempty.of_image₂_left
theorem Finset.Nonempty.of_image₂_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
(Finset.image₂ f s t).Nonempty → s.Nonempty
This theorem states that for any types `α`, `β`, and `γ` and for any binary function `f : α → β → γ`, if `f` is applied to every pair of elements from the finite sets `s` of type `α` and `t` of type `β` to produce a new finite set, and if this new finite set is non-empty, then the original finite set `s` is also non-empty. This basically says that if we have non-empty results from applying a function to pairs from sets `s` and `t`, set `s` cannot be empty.
More concisely: If `f : α → β → γ` is a binary function such that the image of any pair of elements from finite sets `s : α` and `t : β` is a non-empty finite set, then `s` is non-empty.
|
Finset.sup_image₂_left
theorem Finset.sup_image₂_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} (s : Finset α)
(t : Finset β) [inst_1 : SemilatticeSup δ] [inst_2 : OrderBot δ] (g : γ → δ),
(Finset.image₂ f s t).sup g = s.sup fun x => t.sup fun x_1 => g (f x x_1)
This theorem, `Finset.sup_image₂_left`, states that for every two finite sets `s` and `t` of types `α` and `β` respectively, and a binary function `f : α → β → γ`, the supremum (greatest element) of the image of the function over the Cartesian product of `s` and `t`, when mapped to another set via a function `g : γ → δ`, is equal to the supremum of the set obtained by replacing each element of `s` with the supremum of the set obtained by replacing each element of `t` with `g(f x x_1)`. Here, `x` is an element of `s` and `x_1` is an element of `t`.
In mathematical terms, this can be expressed as $\sup \{g(f(a, b)) | a \in s, b \in t\} = \sup \{\sup \{g(f(a, b)) | b \in t\} | a \in s\}$. This is a statement about an interchange of suprema over sets translated using a binary function and a unary function.
More concisely: For finite sets $s$ and $t$ of types $\alpha$ and $\beta$ respectively, and a binary function $f : \alpha \times \beta \to \gamma$, the supremum of $g \circ f$ over the Cartesian product $s \times t$ equals the supremum of $g \circ \sup_t \circ f$ over $s$, where $\sup_t$ is the operation of taking the supremum over the set $t$.
|
Finset.image_image₂_distrib
theorem Finset.image_image₂_distrib :
∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7}
[inst : DecidableEq α'] [inst_1 : DecidableEq β'] [inst_2 : DecidableEq γ] [inst_3 : DecidableEq δ]
{f : α → β → γ} {s : Finset α} {t : Finset β} {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'},
(∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)) →
Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' (Finset.image g₁ s) (Finset.image g₂ t)
This theorem, `Finset.image_image₂_distrib`, states that for all types `α`, `α'`, `β`, `β'`, `γ`, and `δ`, given that `α'`, `β'`, `γ`, and `δ` have decidable equality. If `f` is a binary function from `α` and `β` to `γ`, `s` is a finite set of type `α`, `t` is a finite set of type `β`, `g` is a function from `γ` to `δ`, `f'` is a binary function from `α'` and `β'` to `δ`, `g₁` is a function from `α` to `α'` and `g₂` is a function from `β` to `β'`. If for all `a` in `α` and `b` in `β`, the function `g` of `f(a,b)` is equal to `f'(g₁(a), g₂(b))`, then the image of `g` on the image of `f` over the product set of `s` and `t` is equal to the image of `f'` over the product set of the image of `g₁` on `s` and the image of `g₂` on `t`.
In mathematical terms, it states that the function application and the image operations can be exchanged under certain conditions. This is a distributive property of images of functions over finite sets.
More concisely: If `f: α × β → γ`, `g: γ → δ` are functions, `s ⊆ α` and `t ⊆ β` are finite sets, `g₁: α → α'`, `g₂: β → β'` are functions such that `g(f(a, b)) = f'(g₁(a), g₂(b))` for all `a ∈ α` and `b ∈ β`, then `g(∏ i in s, f(a\_i, b\_i)) = ∏ j in g₁[s], f'(g₁(a\_j), g₂(b\_j))` and `g(∏ i in s, f(a\_i, b\_i)) = ∏ j in g₂[t], f'(g₁(a\_j), g₂(b\_j))`.
|
Finset.image₂_distrib_subset_right
theorem Finset.image₂_distrib_subset_right :
∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {δ : Type u_7} {ε : Type u_9}
[inst : DecidableEq α'] [inst_1 : DecidableEq β'] [inst_2 : DecidableEq δ] [inst_3 : DecidableEq ε] {s : Finset α}
{t : Finset β} {γ : Type u_14} {u : Finset γ} {f : δ → γ → ε} {g : α → β → δ} {f₁ : α → γ → α'} {f₂ : β → γ → β'}
{g' : α' → β' → ε},
(∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)) →
Finset.image₂ f (Finset.image₂ g s t) u ⊆ Finset.image₂ g' (Finset.image₂ f₁ s u) (Finset.image₂ f₂ t u)
The theorem `Finset.image₂_distrib_subset_right` states that for any types `α`, `α'`, `β`, `β'`, `δ`, `ε`, and `γ` and any finite sets `s` of `α`, `t` of `β`, and `u` of `γ`, along with functions `f` from `δ` to `γ` to `ε`, `g` from `α` to `β` to `δ`, `f₁` from `α` to `γ` to `α'`, `f₂` from `β` to `γ` to `β'`, and `g'` from `α'` to `β'` to `ε`, if for all `a` from `α`, `b` from `β`, and `c` from `γ`, the function application `f(g(a,b),c)` equals `g'(f₁(a,c),f₂(b,c))`, then the image of the binary function `f` on the image of `g` over `s` and `t` then `u` is a subset of the image of `g'` over the image of `f₁` over `s` and `u` then the image of `f₂` over `t` and `u`.
More concisely: If `f(g(s,t)) ⊆ g'(f₁(s) ∘ f₂(t)),` where `s` is a finite set of `α, t` is a finite set of `β, u` is a finite set of `γ, f` is a function from `δ` to `γ` to `ε, g` is a function from `α` to `β` to `δ, f₁` is a function from `α` to `γ` to `α', f₂` is a function from `β` to `γ` to `β',` and `g'` is a function from `α'` to `β'` to `ε,` then the image of `f` over `g(s,t)` is a subset of the image of `g'` over `f₁(s) ∘ f₂(t)`.
|
Finset.image₂_union_right
theorem Finset.image₂_union_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α}
{t t' : Finset β} [inst_1 : DecidableEq β],
Finset.image₂ f s (t ∪ t') = Finset.image₂ f s t ∪ Finset.image₂ f s t'
This theorem, `Finset.image₂_union_right`, states that for any types `α`, `β`, and `γ`, where `γ` has decidable equality, given a binary function `f : α → β → γ`, a finite set `s` of type `α`, and two finite sets `t` and `t'` of type `β` with decidable equality, the image of the function `f` over the cartesian product of `s` and the union of `t` and `t'` (denoted as `Finset.image₂ f s (t ∪ t')`) is equal to the union of the image of `f` over `s` and `t` and the image of `f` over `s` and `t'` (denoted as `Finset.image₂ f s t ∪ Finset.image₂ f s t'`).
In mathematical terms, if $f : \alpha \rightarrow \beta \rightarrow \gamma$ is a binary function, $s$ is a finite set of elements of type $\alpha$, and $t$ and $t'$ are finite sets of elements of type $\beta$, then the image of $f$ over the cartesian product of $s$ and the union of $t$ and $t'$ is equal to the union of the image of $f$ over the cartesian products of $s$ and $t$ and of $s$ and $t'$.
More concisely: For any binary function `f` from type `α × β` to type `γ` with decidable equality, finite sets `s` of type `α`, and finite sets `t` and `t'` of type `β`, `Finset.image₂ f (s × (t ∪ t')) = Finset.image₂ f (s × t) ∪ Finset.image₂ f (s × t')`.
|
Finset.image₂_nonempty_iff
theorem Finset.image₂_nonempty_iff :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
(Finset.image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
The theorem `Finset.image₂_nonempty_iff` states that for all types `α`, `β`, and `γ` with `γ` having decidable equality, and for all binary function `f` from `α` and `β` to `γ`, and for all finite sets `s` of type `α` and `t` of type `β`, the image of `f` over `s` and `t` is nonempty if and only if both `s` and `t` are nonempty. In other words, the image of `f` over the Cartesian product of `s` and `t` has at least one element if and only if both `s` and `t` have at least one element.
More concisely: For all types `α`, `β`, and `γ` with decidable equality, and for all binary functions `f` from `α × β` to `γ`, the image of `f` over a finite set `s` of type `α` and `t` of type `β` is nonempty if and only if both `s` and `t` are nonempty.
|
Finset.card_image₂_iff
theorem Finset.card_image₂_iff :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
(Finset.image₂ f s t).card = s.card * t.card ↔ Set.InjOn (fun x => f x.1 x.2) (↑s ×ˢ ↑t)
The theorem `Finset.card_image₂_iff` states that for any types α, β, and γ with decidable equality over γ, any binary function `f` from α and β to γ, and any finite sets `s` of α and `t` of β, the cardinality of the image of the function `f` over `s` and `t` is equal to the product of the cardinalities of `s` and `t` if and only if the function `f` is injective on the cartesian product of `s` and `t`. In simpler terms, if every unique pair of elements from `s` and `t` maps to a unique value in γ (i.e., `f` doesn't map any two different pairs to the same value), then the total number of such unique values is exactly the number of elements in `s` times the number of elements in `t`.
More concisely: The cardinality of the image of a function from two finite sets to a type with decidable equality is equal to the product of their cardinalities if and only if the function is injective on their cartesian product.
|
Set.toFinset_image2
theorem Set.toFinset_image2 :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] (f : α → β → γ) (s : Set α) (t : Set β)
[inst_1 : Fintype ↑s] [inst_2 : Fintype ↑t] [inst_3 : Fintype ↑(Set.image2 f s t)],
(Set.image2 f s t).toFinset = Finset.image₂ f s.toFinset t.toFinset
This theorem states that for all types `α`, `β`, and `γ` with `γ` having a decidable equality, and for all functions `f` from `α` and `β` to `γ`, and sets `s` of `α` and `t` of `β`, given that `s`, `t`, and the image of the binary function `f` on `s` and `t` are finite, the finset constructed from the image of `f` on `s` and `t` is equal to the image of the binary function `f` on the finsets constructed from `s` and `t`. In mathematical terms, this can be interpreted as the image of a binary function on two sets being the same as the image of the function on the corresponding finite sets.
More concisely: Given types `α`, `β`, and `γ` with decidable equality, finite sets `s` of `α` and `t` of `β`, and a function `f` from `α` and `β` to `γ`, the image of `f` on the finsets `s` and `t` is equal to the finset of `γ` obtained by applying `f` to each element in the Cartesian product `s × t`.
|
Finset.image₂_subset
theorem Finset.image₂_subset :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s s' : Finset α}
{t t' : Finset β}, s ⊆ s' → t ⊆ t' → Finset.image₂ f s t ⊆ Finset.image₂ f s' t'
This theorem states that for all types `α`, `β`, and `γ` where `γ` has decidable equality, and for any binary function `f` from `α` and `β` to `γ`, if we have two subsets `s` and `t` of `α` and `β` respectively, and these subsets are included in larger sets `s'` and `t'` respectively (`s ⊆ s'` and `t ⊆ t'`), then the image of the binary function `f` applied to the smaller subsets is also included in the image of the same function applied to the larger sets (`Finset.image₂ f s t ⊆ Finset.image₂ f s' t'`). In mathematical terms, it expresses the property that the image of a function is monotone with respect to set inclusion.
More concisely: For any function between two sets with decidable equality and a decidable image, the image of two included sets is included in the image of their supersets.
|
Finset.image_image₂_right_anticomm
theorem Finset.image_image₂_right_anticomm :
∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq β']
[inst_1 : DecidableEq γ] [inst_2 : DecidableEq δ] {s : Finset α} {t : Finset β} {f : α → β' → γ} {g : β → β'}
{f' : β → α → δ} {g' : δ → γ},
(∀ (a : α) (b : β), f a (g b) = g' (f' b a)) →
Finset.image₂ f s (Finset.image g t) = Finset.image g' (Finset.image₂ f' t s)
This theorem, `Finset.image_image₂_right_anticomm`, states that for any types `α`, `β`, `β'`, `γ`, `δ`, any finite sets `s` of type `α` and `t` of type `β`, any binary function `f` from `α` and `β'` to `γ`, any function `g` from `β` to `β'`, any binary function `f'` from `β` and `α` to `δ`, and any function `g'` from `δ` to `γ`, such that for every element `a` of type `α` and `b` of type `β`, `f(a, g(b)) = g'(f'(b, a))`, then the image of the binary function `f` applied to `s` and the image of `g` applied to `t` is equal to the image of `g'` applied to the image of the binary function `f'` applied to `t` and `s`. In other words, this theorem asserts a kind of "commutativity" property for operations on images of functions over finite sets.
More concisely: For any functions `f : α × β' → γ`, `g : β → β'`, `f' : β × α → δ`, and `g' : δ → γ` satisfying `f(a, g(b)) = g'(f'(b, a))` for all `a : α` and `b : β`, the image of `f` applied to a finite set `s` of type `α` and the image of `g` applied to a finite set `t` of type `β` is equal to the image of `g'` applied to the image of `f'` applied to `t` and `s`.
|
Finset.image_image₂_distrib_right
theorem Finset.image_image₂_distrib_right :
∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq β']
[inst_1 : DecidableEq γ] [inst_2 : DecidableEq δ] {f : α → β → γ} {s : Finset α} {t : Finset β} {g : γ → δ}
{f' : α → β' → δ} {g' : β → β'},
(∀ (a : α) (b : β), g (f a b) = f' a (g' b)) →
Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' s (Finset.image g' t)
This theorem, `Finset.image_image₂_distrib_right`, states that for any types `α`, `β`, `β'`, `γ`, and `δ`, with decidable equality on `β'`, `γ`, and `δ`, and for any binary functions `f : α → β → γ`, `f' : α → β' → δ`, and unary functions `g : γ → δ`, `g' : β → β'`, if for all `α`, `β`, the function `g` composed with `f` equals `f'` composed with `a` and `g'` with `b`, then the image of `g` over the image₂ of `f` over `s` and `t` is equal to the image₂ of `f'` over `s` and the image of `g'` over `t`. In mathematical terms, this confirms the commutativity of the diagram involving these functions and sets.
More concisely: For functions `f : α → β → γ`, `f' : α → β' → δ`, `g : γ → δ`, and `g' : β → β'`, with decidable equality on `β'`, `γ`, and `δ`, if `g ∘ f = f' ∘ a ∘ g'`, then `image₂ f (image₂ a s t) = image₂ f' (image s t)`.
|
Finset.image₂_congr'
theorem Finset.image₂_congr' :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f f' : α → β → γ} {s : Finset α}
{t : Finset β}, (∀ (a : α) (b : β), f a b = f' a b) → Finset.image₂ f s t = Finset.image₂ f' s t
This theorem, `Finset.image₂_congr'`, states that for any types `α`, `β`, and `γ` where `γ` has decidable equality, for any two binary functions `f` and `f'` from `α` and `β` to `γ`, and for any finite sets `s` of type `α` and `t` of type `β`; if for every element `a` of `α` and `b` of `β`, `f a b` equals `f' a b`, then the image of the function `f` over the Cartesian product of sets `s` and `t` equals the image of the function `f'` over the same Cartesian product. In mathematical terms, if $f(a, b) = f'(a, b)$ for all $a \in \alpha$ and $b \in \beta$, then the image of $f$ over $s \times t$ equals the image of $f'$ over $s \times t$.
More concisely: If `α`, `β`, and `γ` are types with decidable equality and `f` and `f'` are binary functions from `α` to `β` to `γ`, then `f''(s × t) = f'(s × t)` where `f''(a, b) = f a b` and `f'(a, b)` are their respective images on the Cartesian product of finite sets `s` and `t`.
|
Finset.card_image₂_le
theorem Finset.card_image₂_le :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] (f : α → β → γ) (s : Finset α) (t : Finset β),
(Finset.image₂ f s t).card ≤ s.card * t.card
This theorem states that for any types `α`, `β`, and `γ`, given a binary function `f` from `α` and `β` to `γ`, and finite sets `s` of type `α` and `t` of type `β`, the cardinality (or size) of the image set formed by applying the function `f` to every pair of elements in `s` and `t` is less than or equal to the product of the cardinalities of `s` and `t`. This can be interpreted as a form of the Pigeonhole principle: if we map each possible pair of elements from two sets into another set, we can't have more unique results than the total number of pairs. The equality in `γ` is assumed to be decidable.
More concisely: For any finite sets $s$ of type $\alpha$, $t$ of type $\beta$, and assuming decidable equality in $\gamma$, the number of elements in the image of the binary function $f : \alpha \times \beta \rightarrow \gamma$ applied to all pairs in $s \times t$ is less than or equal to the product of the cardinalities of $s$ and $t$.
|
Finset.image₂_left_identity
theorem Finset.image₂_left_identity :
∀ {α : Type u_1} {γ : Type u_5} [inst : DecidableEq γ] {f : α → γ → γ} {a : α},
(∀ (b : γ), f a b = b) → ∀ (t : Finset γ), Finset.image₂ f {a} t = t
This theorem states that for any types `α` and `γ` with `γ` having a decidable equality, given a function `f` from `α` to `γ → γ` and an element `a` of `α`, if `a` acts as a left identity for `f` (which means that for any `b` in `γ`, `f a b = b`), then the singleton set `{a}` is a left identity for the binary function `Finset.image₂ f`. In other words, for any finite set `t` of `γ`, applying `Finset.image₂ f` to `{a}` and `t` gives `t` back; the operation leaves `t` unchanged.
More concisely: For any types `α` and `γ` with decidable equality, if `f: α → γ → γ` is a function and `a ∈ α` is an element such that `f a b = b` for all `b ∈ γ`, then the singleton set `{a} ⊆ α` is a left identity for `Finset.image₂ f`, i.e., `Finset.image₂ f ({a}, _) = _`.
|
Finset.biUnion_image_right
theorem Finset.biUnion_image_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
(t.biUnion fun b => Finset.image (fun a => f a b) s) = Finset.image₂ f s t
The theorem `Finset.biUnion_image_right` states that for any types `α`, `β`, and `γ` with `γ` having decidable equality, and given a binary function `f : α → β → γ` and two finite sets `s : Finset α` and `t : Finset β`, the biUnion of `t` with the function that applies `f` to each element of `s` and a fixed element of `t` (i.e. `(Finset.biUnion t fun b => Finset.image (fun a => f a b) s)`) is equivalent to the image of `f` over the Cartesian product of `s` and `t` (i.e. `Finset.image₂ f s t`). This means that the set of all values obtained by applying `f` to pairs `(a, b)` where `a` is from `s` and `b` is from `t` can be computed in either of these two ways.
More concisely: For finite sets `s : Finset α` and `t : Finset β`, and a binary function `f : α → β → γ` with `γ` having decidable equality, the biUnion of `t` with the function `Finset.image (fun a => f a <$> t) s` is equal to the image of `f` over the Cartesian product `s × t` (`Finset.image₂ f s t`).
|
Finset.image₂_image_left_comm
theorem Finset.image₂_image_left_comm :
∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq α']
[inst_1 : DecidableEq γ] [inst_2 : DecidableEq δ] {s : Finset α} {t : Finset β} {f : α' → β → γ} {g : α → α'}
{f' : α → β → δ} {g' : δ → γ},
(∀ (a : α) (b : β), f (g a) b = g' (f' a b)) →
Finset.image₂ f (Finset.image g s) t = Finset.image g' (Finset.image₂ f' s t)
This theorem, `Finset.image₂_image_left_comm`, states that for any given types `α`, `α'`, `β`, `γ`, and `δ`, and any two functions `f : α' -> β -> γ` and `g : α -> α'`, and any function `f' : α -> β -> δ` and `g' : δ -> γ`, and given two sets `s : Finset α` and `t : Finset β`, if for all `a` in `α` and `b` in `β`, `f (g a) b` equals `g' (f' a b)`, then the image of the binary function `f` over the image of `g` on the set `s` and the set `t` is the same as the image of `g'` on the binary image of `f'` over `s` and `t`. In other words, if the functions `f`, `g`, `f'` and `g'` satisfy a particular relationship, then the images of these functions over the sets `s` and `t` follow a certain commutative property.
More concisely: If functions `f : α' -> β -> γ`, `g : α -> α'`, `f' : α -> β -> δ`, and `g' : δ -> γ` satisfy `f (g a) b = g' (f' a b)` for all `a in α` and `b in β`, then `(g '' s) `` image f `` t = g' `` image (f' `' s) t`.
|
Finset.image₂_inter_subset_left
theorem Finset.image₂_inter_subset_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s s' : Finset α}
{t : Finset β} [inst_1 : DecidableEq α],
Finset.image₂ f (s ∩ s') t ⊆ Finset.image₂ f s t ∩ Finset.image₂ f s' t
The theorem `Finset.image₂_inter_subset_left` states that, for any types `α`, `β`, and `γ` with `γ` having decidable equality, for any binary function `f` from `α` and `β` to `γ`, for any finite sets `s`, `s'` of `α`, and `t` of `β`, with `α` having decidable equality, the image under `f` of the intersection of `s` and `s'` with `t` is a subset of the intersection of the images under `f` of `s` with `t` and `s'` with `t`.
In mathematical terms, this is saying that given a function `f: α × β → γ`, and finite sets `s, s' ⊆ α`, `t ⊆ β`, we have `f((s ∩ s') × t) ⊆ f(s × t) ∩ f(s' × t)`. Here, `f(S × T)` for sets `S ⊆ α` and `T ⊆ β` denotes the image of the cartesian product `S × T` under the function `f`.
More concisely: For any function $f:\alpha \times \beta \to \gamma$ with $\gamma$ having decidable equality, and finite sets $s, s' \subseteq \alpha$, $t \subseteq \beta$ of type $\alpha$ with decidable equality, we have $f((s \cap s') \times t) \subseteq f(s \times t) \cap f(s' \times t)$.
|
Finset.coe_image₂
theorem Finset.coe_image₂ :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] (f : α → β → γ) (s : Finset α) (t : Finset β),
↑(Finset.image₂ f s t) = Set.image2 f ↑s ↑t
This theorem states that for any types `α`, `β`, `γ` and a binary function `f` from `α` and `β` to `γ`, for any finite sets `s` of type `α` and `t` of type `β`, the image of `f` over the cartesian product of `s` and `t` (obtained using `Finset.image₂` and then coerced to a set) is equal to the image of `f` over the cartesian product of `s` and `t` considered as sets (obtained using `Set.image2`). This equality holds when we have a decidable equality on `γ`. In other words, the theorem reveals the consistency between the `image₂` operations on finite sets and on general sets when we view finite sets as particular sets.
More concisely: For any types `α`, `β`, `γ` and a decidably equated binary function `f` from `α × β` to `γ`, the sets `Finset.image₂ f (Finset.univ s) (Finset.univ t)` and `Set.image2 f (s × t)` are equal, where `s` is a finite set of type `α` and `t` is a finite set of type `β`.
|
Finset.image₂_eq_empty_iff
theorem Finset.image₂_eq_empty_iff :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
Finset.image₂ f s t = ∅ ↔ s = ∅ ∨ t = ∅
This theorem states that for any types `α`, `β`, and `γ` where `γ` has decidable equality, given a binary function `f : α → β → γ` and two finite sets `s : Finset α` and `t : Finset β`, the image of the function `f` applied to `s` and `t` results in an empty set if and only if either `s` or `t` (or both) are empty. In other words, when you apply a function to every combination of elements from two sets, if the resulting set is empty, then at least one of the original sets was empty.
More concisely: For functions between types with decidable equality, the image of a binary function applied to two finite sets is empty if and only if at least one of the sets is empty.
|
Finset.image₂_subset_iff
theorem Finset.image₂_subset_iff :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
{u : Finset γ}, Finset.image₂ f s t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u
This theorem provides a condition to determine whether the image of a binary function `f : α → β → γ` over two finite sets `s : Finset α` and `t : Finset β` is a subset of another finite set `u : Finset γ` in a type with decidable equality. Specifically, it states that the image of `f` over `s` and `t` is a subset of `u` if and only if for every element `x` in `s` and every element `y` in `t`, the result `f x y` is an element of `u`.
More concisely: For finite sets `s`, `t`, and `u`, and a binary function `f : α → β → γ`, `f (s : Finset α) (t : Finset β) ⊆ u : Finset γ` if and only if for all `x ∈ s` and `y ∈ t`, `f x y ∈ u`.
|
Finset.subset_image₂
theorem Finset.subset_image₂ :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {u : Finset γ} {s : Set α}
{t : Set β}, ↑u ⊆ Set.image2 f s t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ Finset.image₂ f s' t'
This theorem states that for any types `α`, `β`, and `γ` with a decidable equality relation on `γ`, given a binary function `f` from `α` and `β` to `γ`, a `Finset` of `γ` named `u`, and two sets `s` and `t` of types `α` and `β` respectively, if `u` is a subset of the image of `s` and `t` under the function `f`, then there exist `Finset` subsets `s'` and `t'` of `s` and `t` respectively such that `u` is a subset of the image of `s'` and `t'` under the function `f`. In mathematical terms, if $u \subseteq f(s, t)$, then there must exist $s' \subseteq s$ and $t' \subseteq t$ such that $u \subseteq f(s', t')$.
More concisely: Given types `α`, `β`, and `γ` with decidable equality on `γ`, if `Finset` `u` is a subset of the image of sets `s` of type `α` and `t` of type `β` under a binary function `f` from `α` and `β` to `γ`, then there exist subsets `s'` of `s` and `t'` of `t` such that `u` is a subset of the image of `s'` and `t'` under `f`.
|
Finset.card_dvd_card_image₂_right
theorem Finset.card_dvd_card_image₂_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
(∀ a ∈ s, Function.Injective (f a)) →
((fun a => Finset.image (f a) t) '' ↑s).PairwiseDisjoint id → t.card ∣ (Finset.image₂ f s t).card
The theorem `Finset.card_dvd_card_image₂_right` states that for any types `α`, `β`, `γ` and a function `f : α → β → γ`, and finite sets `s : Finset α` and `t : Finset β`, given that each partial application of the function `f` with elements in `s` is injective, and the images of `s` under those partial applications are pairwise disjoint, then the size of `t` divides the size of the image of the binary function `f` applied to `s` and `t`. In simpler terms, if we apply `f` to each pair of elements from `s` and `t` and the results do not overlap, then the number of elements in `t` will be a divisor of the total number of outcomes.
More concisely: If `f : α → β → γ`, `s : Finset α`, `t : Finset β` satisfy that `f` restricted to pairs of elements from `s` and `t` is injective and the images are disjoint, then `#t` divides `#(image (λ x, λ y, f x y) s)`.
|
Finset.card_image₂_singleton_left
theorem Finset.card_image₂_singleton_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} (t : Finset β) {a : α},
Function.Injective (f a) → (Finset.image₂ f {a} t).card = t.card
This theorem states that, given any types `α`, `β`, and `γ`, along with an instance of decidable equality for `γ`, a binary function `f` from `α` to `β` to `γ`, a finite set `t` of type `β`, and an element `a` of type `α`, if the function `f` applied to `a` is injective (meaning that it produces a unique output for each unique input), then the size (cardinality) of the image of `f` when applied to the singleton set `{a}` and `t` is equal to the size of `t`.
In other words, when an injective function is applied to a singleton set and another set, it will produce a new set with the same number of elements as the second set.
This theorem is essentially asserting a property of injective functions: they preserve the number of distinct elements when mapping from one set to another.
More concisely: Given an injective function from a set to a finite set and a singleton set, the size of the image of the singleton set equals the size of the target set.
|
Finset.image₂_swap
theorem Finset.image₂_swap :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] (f : α → β → γ) (s : Finset α) (t : Finset β),
Finset.image₂ f s t = Finset.image₂ (fun a b => f b a) t s
The theorem `Finset.image₂_swap` states that for any types `α`, `β`, and `γ` and for any binary function `f` from `α` and `β` to `γ`, and for any finite sets `s` of type `α` and `t` of type `β`, applying the image of `f` over `s` and `t` is the same as applying the image of the swapped version of `f` over `t` and `s`. In other words, the order of the sets in the image operation does not affect the result when the arguments of the function are swapped. This operation is equivalent in natural language to swapping the order of the two sets in the Cartesian product and then applying the swapped function.
More concisely: For any finite sets $s$ of type $\alpha$, $t$ of type $\beta$, and binary function $f$ from $\alpha$ and $\beta$ to $\gamma$, $f(s \times t) = f(t \times s)$.
|
Finset.image₂_right_comm
theorem Finset.image₂_right_comm :
∀ {α : Type u_1} {β : Type u_3} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} [inst : DecidableEq δ]
[inst_1 : DecidableEq δ'] [inst_2 : DecidableEq ε] {s : Finset α} {t : Finset β} {γ : Type u_14} {u : Finset γ}
{f : δ → γ → ε} {g : α → β → δ} {f' : α → γ → δ'} {g' : δ' → β → ε},
(∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b) →
Finset.image₂ f (Finset.image₂ g s t) u = Finset.image₂ g' (Finset.image₂ f' s u) t
The theorem `Finset.image₂_right_comm` states that for all types `α`, `β`, `δ`, `δ'`, `ε`, `γ`, given two binary functions `f : δ → γ → ε` and `g : α → β → δ`, a third binary function `f' : α → γ → δ'`, a fourth binary function `g' : δ' → β → ε`, and three finite sets `s : Finset α`, `t : Finset β`, and `u : Finset γ`, if for every `a` in `α`, `b` in `β`, and `c` in `γ`, `f` applied to `g` of `a` and `b` and `c` equals `g'` applied to `f'` of `a` and `c` and `b`, then the image of `f` over the cartesian product of the image of `g` over the cartesian product of `s` and `t` and `u` equals the image of `g'` over the cartesian product of the image of `f'` over the cartesian product of `s` and `u` and `t`.
In simpler terms, the theorem says that if `f` and `g'` commute under certain conditions and `g` and `f'` play a similar role, then the image sets obtained by these functions on the given finite sets will also commute.
More concisely: If functions `f`, `g`, `f'`, and `g'` satisfy `f(g(x, y)) = g'(f'(x, y))` for all `x` in the domain of `f'` and `y` in the domain of `g`, then the images of `f` and `g'` over the cartesian products of their respective domains and finite sets `s`, `t`, and `u` commute.
|
Set.Finite.toFinset_image2
theorem Set.Finite.toFinset_image2 :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {s : Set α} {t : Set β} (f : α → β → γ)
(hs : s.Finite) (ht : t.Finite) (hf : optParam (Set.image2 f s t).Finite ⋯),
Set.Finite.toFinset hf = Finset.image₂ f hs.toFinset ht.toFinset
The theorem `Set.Finite.toFinset_image2` states that for any types `α`, `β`, `γ` with a decidable equality on `γ`, any finite sets `s` of type `α` and `t` of type `β`, and a binary function `f : α → β → γ`, the `Finset` (i.e., a finite set with no duplicates) that represents the image of the function `f` applied to `s` and `t` (denoted `Set.image2 f s t`) is equal to the image of `f` applied to the `Finset` representations of `s` and `t`. This is under the assumption that the image `Set.image2 f s t` is finite, which is an optional parameter `hf` in the theorem.
More concisely: For any types `α`, `β`, `γ` with decidable equality, finite sets `s : Finset α`, `t : Finset β`, and a binary function `f : α → β → γ`, if `Set.image2 f s t` is finite, then `Set.image2 f s t = Set.image (λ x y, f x y) (Set.unioneq s (Set.map Set.fst t))`.
|
Finset.image_image₂_antidistrib_left
theorem Finset.image_image₂_antidistrib_left :
∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq β']
[inst_1 : DecidableEq γ] [inst_2 : DecidableEq δ] {f : α → β → γ} {s : Finset α} {t : Finset β} {g : γ → δ}
{f' : β' → α → δ} {g' : β → β'},
(∀ (a : α) (b : β), g (f a b) = f' (g' b) a) →
Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' (Finset.image g' t) s
This theorem, `Finset.image_image₂_antidistrib_left`, states that for all types `α`, `β`, `β'`, `γ`, and `δ`, with `β'`, `γ`, and `δ` having decidable equality, given a binary function `f` from `α` and `β` to `γ`, two finite sets `s` and `t` of types `α` and `β` respectively, a function `g` from `γ` to `δ`, another binary function `f'` from `β'` and `α` to `δ`, and a function `g'` from `β` to `β'`, if for all `α` and `β`, the function `g` applied to `f` of `α` and `β` equals `f'` of `g'` of `β` and `α`, then the image of `g` on the image of `f` on `s` and `t` is equal to the image of `f'` on the image of `g'` on `t` and `s`. In mathematical terms, if $g(f(a, b)) = f'(g'(b), a)$ for all $a$ and $b$, then $g(f(S, T)) = f'(g'(T), S)$.
More concisely: If for all pairs (a, b) in the product of two finite sets, g(f(a, b)) = f'(g'(b), a), then g(Image(f)(S)) = Image(f')(Image(g')(S)) for any finite sets S in α.
|
Finset.image₂_distrib_subset_left
theorem Finset.image₂_distrib_subset_left :
∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ' : Type u_6} {δ : Type u_7} {ε : Type u_9}
[inst : DecidableEq β'] [inst_1 : DecidableEq γ'] [inst_2 : DecidableEq δ] [inst_3 : DecidableEq ε] {s : Finset α}
{t : Finset β} {γ : Type u_14} {u : Finset γ} {f : α → δ → ε} {g : β → γ → δ} {f₁ : α → β → β'} {f₂ : α → γ → γ'}
{g' : β' → γ' → ε},
(∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)) →
Finset.image₂ f s (Finset.image₂ g t u) ⊆ Finset.image₂ g' (Finset.image₂ f₁ s t) (Finset.image₂ f₂ s u)
This theorem states that for any types `α`, `β`, `β'`, `γ'`, `δ`, `ε`, and `γ`, and given finsets `s`, `t`, and `u` of these types, along with functions `f : α → δ → ε`, `g : β → γ → δ`, `f₁ : α → β → β'`, `f₂ : α → γ → γ'`, and `g' : β' → γ' → ε`, if for all elements `a` of `α`, `b` of `β`, and `c` of `γ`, `f a (g b c)` equals to `g' (f₁ a b) (f₂ a c)`, then the image of the binary function `f` over the set `s` and the image of the binary function `g` over the sets `t` and `u` is a subset of the image of the binary function `g'` over the image of the binary function `f₁` over the sets `s` and `t` and the image of the binary function `f₂` over the sets `s` and `u`. The theorem is establishing a specific kind of relationship between these binary functions and the subsets of their ranges.
More concisely: If for all `a` in `α`, `b` in `β`, and `c` in `γ`, `f a (g b c) = g' (f₁ a b) (f₂ a c)` implies the image of `f` over sets `s` and `t` and image of `g` over sets `u`, `t`, and `v` is a subset of the image of `g'` over the images of `f₁` and `f₂` on sets `s`, `t`, and `s`, `u`, respectively.
|
Finset.card_dvd_card_image₂_left
theorem Finset.card_dvd_card_image₂_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
(∀ b ∈ t, Function.Injective fun a => f a b) →
((fun b => Finset.image (fun a => f a b) s) '' ↑t).PairwiseDisjoint id → s.card ∣ (Finset.image₂ f s t).card
The theorem `Finset.card_dvd_card_image₂_left` states that for any types `α`, `β`, and `γ` with decidable equality on `γ`, given a binary function `f : α → β → γ`, and two finite sets `s : Finset α` and `t : Finset β`, if every partial application of `f` (fixing the second argument in `t`) is an injective function, and the images of `t` under these partial applications are pairwise disjoint (meaning, the sets of images don't overlap, but are not necessarily distinct), then the cardinality (or size) of `s` divides the cardinality of the image of `s` and `t` under `f`. In terms of sets, this is saying that the size of `s` is a factor of the size of the set obtained by applying `f` to each pair of elements from `s` and `t`.
More concisely: If `f : α → β → γ` is a function with decidable equality on `γ`, `s : Finset α`, and `t : Finset β` such that for all `a in s` and `b, c in t`, `a = a` implies `f a b = f a c` and the images of `t` under these partial applications are disjoint, then `#s` divides `#(map (λ x, map (λ y, f x y) t) s)`.
|
Finset.image_uncurry_product
theorem Finset.image_uncurry_product :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] (f : α → β → γ) (s : Finset α) (t : Finset β),
Finset.image (Function.uncurry f) (s ×ˢ t) = Finset.image₂ f s t
The theorem `Finset.image_uncurry_product` asserts that for any types `α`, `β`, and `γ`, where equality in `γ` is decidable, and given a binary function `f : α → β → γ`, and finite sets `s : Finset α` and `t : Finset β`, the image of the uncurried function `Function.uncurry f` over the cartesian product of `s` and `t` is equivalent to the image of the function `f` computed via `Finset.image₂`. In other words, it asserts the equality of two different ways to compute the forward image of a binary function over a pair of finite sets.
More concisely: For any decidably-equaled types `α`, `β`, `γ`, and finite sets `s : Finset α` and `t : Finset β`, the image of the uncurried function `Function.uncurry (α × β → γ)` over `s × t` equals the image of the original function `α × β → γ` applied to `Finset.image₂ s t`.
|
Finset.image₂_singleton
theorem Finset.image₂_singleton :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {a : α} {b : β},
Finset.image₂ f {a} {b} = {f a b}
The theorem `Finset.image₂_singleton` states that for any types `α`, `β`, and `γ` where `γ` has decidable equality, given a binary function `f : α → β → γ` and elements `a : α` and `b : β`, the image of the function `f` when applied to the singleton sets `{a}` and `{b}` (denoted as `Finset.image₂ f {a} {b}`) is a singleton set containing the value `f a b`, i.e., `{f a b}`. This essentially means that applying a binary function to two singleton sets results in a singleton set of the function applied to the elements of these sets.
More concisely: For any types `α`, `β`, and `γ` with decidable equality, the image of a binary function `f : α → β → γ` on singleton sets `{a : α}` and `{b : β}` is the singleton set `{f a b : γ}` containing the result `f a b`.
|
Finset.mem_image₂
theorem Finset.mem_image₂ :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
{c : γ}, c ∈ Finset.image₂ f s t ↔ ∃ a ∈ s, ∃ b ∈ t, f a b = c
The theorem `Finset.mem_image₂` states that for any types `α`, `β`, and `γ` with a decidable equality operation on `γ`, and any binary function `f : α → β → γ`, finite sets `s : Finset α` and `t : Finset β`, and an element `c : γ`, that element `c` is in the image of the binary function `f` applied across the Cartesian product of sets `s` and `t` if and only if there exist elements `a` in `s` and `b` in `t` such that applying `f` to `a` and `b` yields `c`. In mathematical terms, $c \in Im(f; s \times t)$ if and only if $\exists a \in s, b \in t : f(a, b) = c$.
More concisely: The theorem asserts that an element is in the image of a binary function applied to the Cartesian product of two finite sets if and only if there exist elements in each set whose application of the function results in that element.
|
Finset.inf_image₂_right
theorem Finset.inf_image₂_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} (s : Finset α)
(t : Finset β) [inst_1 : SemilatticeInf δ] [inst_2 : OrderTop δ] (g : γ → δ),
(Finset.image₂ f s t).inf g = t.inf fun y => s.inf fun x => g (f x y)
The theorem `Finset.inf_image₂_right` states that for any finite sets `s` of type `α` and `t` of type `β`, a function `f` mapping elements from `α` and `β` to `γ`, and a function `g` mapping elements from `γ` to a structure `δ` with an infimum and a top element, the infimum of the image of `g` applied to the set obtained by `f` acting on the Cartesian product of `s` and `t` is equal to the infimum over `t` of the infimum over `s` of `g` applied to `f` acting on each pair of elements in `s` and `t`. In mathematical terms, the theorem states that $\inf_{(x,y) \in s \times t} g(f(x, y)) = \inf_{y \in t} \inf_{x \in s} g(f(x, y))$.
More concisely: The infimum of the image of a function `g` over the Cartesian product of sets `s` and `t`, applied to the pairwise applications of a function `f` from `s` to `β` and `t` to `α`, equals the infimum over `t` of the infima over `s` of `g` applied to `f(x, y)` for each `x` in `s` and `y` in `t`.
|
Finset.image₂_subset_right
theorem Finset.image₂_subset_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s s' : Finset α}
{t : Finset β}, s ⊆ s' → Finset.image₂ f s t ⊆ Finset.image₂ f s' t
The theorem `Finset.image₂_subset_right` states that for any types `α`, `β`, and `γ`, with `γ` having decidable equality, and any function `f` from `α` and `β` to `γ`, if one finite set `s` of type `α` is a subset of another finite set `s'` of the same type, and `t` is a finite set of type `β`, then the image of the binary function `f` applied to the pairs from `s` and `t` is a subset of the image of `f` applied to the pairs from `s'` and `t`. In other words, if `s` is a subset of `s'`, then the set of all values `f(a, b)` for `a` in `s` and `b` in `t` is a subset of the set of all values `f(a', b)` for `a'` in `s'` and `b` in `t`.
More concisely: If `s` is a subset of `s'` in type `α`, and `t` is a finite set of type `β`, then the image of the function `f` from `α × β` to `γ` applied to pairs in `s × t` is a subset of the image of `f` applied to pairs in `s' × t`, where `γ` has decidable equality.
|
Mathlib.Data.Finset.NAry._auxLemma.2
theorem Mathlib.Data.Finset.NAry._auxLemma.2 :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
{c : γ}, (c ∈ Finset.image₂ f s t) = ∃ a ∈ s, ∃ b ∈ t, f a b = c
This theorem states that for all sets `s` of type `α`, `t` of type `β`, and a function `f` mapping elements from `α` and `β` to `γ`, where `γ` has decidable equality, an element `c` of type `γ` belongs to the image of `f` applied to the cartesian product of `s` and `t` if and only if there exist elements `a` in `s` and `b` in `t` such that `f` applied to `a` and `b` equals `c`. In other words, this theorem is about the membership of an element in the image of a binary function applied to two sets.
More concisely: For sets `s` of type `α`, `t` of type `β`, and a total function `f` from `α × β` to `γ`, an element `c` of type `γ` is in the image of `f` applied to the cartesian product of `s` and `t` if and only if there exist `a` in `s` and `b` in `t` such that `f`(`a`, `b`) = `c`.
|
Finset.image₂_singleton_left
theorem Finset.image₂_singleton_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {t : Finset β} {a : α},
Finset.image₂ f {a} t = Finset.image (fun b => f a b) t
This theorem, `Finset.image₂_singleton_left`, states that for all types `α`, `β`, and `γ` where `γ` has decidable equality, for any binary function `f : α → β → γ`, any finite set `t : Finset β`, and any value `a : α`, the image of the function `f` when applied to the singleton finite set containing only `a` and the finite set `t` is equal to the image of the function `(fun b => f a b)` when applied to the finite set `t`. In mathematical terms, it asserts that applying `f` to the Cartesian product of `{a}` and `t` is the same as mapping `f a` over `t`.
More concisely: For any types `α`, `β`, and `γ` with decidable equality, and for any binary function `f : α → β → γ`, the image of `f` applied to the singleton set `{a}` and finite set `t` is equal to the image of the function `x mapsto f a x` applied to `t`.
|
Finset.image_subset_image₂_left
theorem Finset.image_subset_image₂_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
{b : β}, b ∈ t → Finset.image (fun a => f a b) s ⊆ Finset.image₂ f s t
The theorem `Finset.image_subset_image₂_left` states that for any types `α`, `β`, and `γ` with decidable equality on `γ`, and for any binary function `f : α → β → γ`, any finite sets `s : Finset α` and `t : Finset β`, and any element `b : β` in `t`, the image of the set `s` under the function `a => f a b` is a subset of the image of the set `s × t` under the function `f`. In other words, applying the function `f` to each element of `s` and a fixed value `b` from `t` results in a set that is contained within the set obtained by applying `f` to all pairs `(a, b')` where `a` is from `s` and `b'` is from `t`.
More concisely: For any decidably equal types `α`, `β`, and `γ`, and decidable `β-values` `b`, the image of a finite set `s ∈ Finset α` under the function `f : α × β → γ` is a subset of the image of the product set `s × {b} ∈ Finset (α × β)` under the same function `f`.
|
Mathlib.Data.Finset.NAry._auxLemma.7
theorem Mathlib.Data.Finset.NAry._auxLemma.7 :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β},
(Finset.image f s ⊆ t) = ∀ x ∈ s, f x ∈ t
This theorem, `Mathlib.Data.Finset.NAry._auxLemma.7`, states that for all types `α` and `β`, given a function `f` from `α` to `β`, a finite set `s` of type `α`, and a finite set `t` of type `β`, with `β` having decidable equality, the forward image of `s` under `f` being a subset of `t` is equivalent to the statement that for every element `x` in `s`, the function `f` applied to `x` is an element of `t`. In other words, every element of the image of `s` under `f` must belong to `t`.
More concisely: For all types `α` and `β` with decidable equality, given a function `f` from `α` to `β`, a finite set `s` of type `α`, and a finite set `t` of type `β`, the image of `s` under `f` is a subset of `t` if and only if for all `x` in `s`, `f(x)` is in `t`.
|
Finset.Nonempty.of_image₂_right
theorem Finset.Nonempty.of_image₂_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
(Finset.image₂ f s t).Nonempty → t.Nonempty
The theorem `Finset.Nonempty.of_image₂_right` states that, for any types `α`, `β`, and `γ` with `γ` having decidable equality, and given a binary function `f` from `α` and `β` to `γ`, and two finite sets `s` and `t` of types `α` and `β` respectively, if the image of the function `f` over the Cartesian product of `s` and `t` is nonempty, then `t` is also nonempty. In mathematical terms, if there exists at least one element in the set ${f(a,b) | a ∈ s, b ∈ t}$, then there exists at least one element in set `t`.
More concisely: If `f` is a binary function from types `α` and `β` to a type `γ` with decidable equality, and the image of `f` over the Cartesian product of nonempty finite sets `s` and `t` of types `α` and `β` respectively is nonempty, then `t` is nonempty.
|
Finset.forall_image₂_iff
theorem Finset.forall_image₂_iff :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
{p : γ → Prop}, (∀ z ∈ Finset.image₂ f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)
The theorem `Finset.forall_image₂_iff` states that for all types `α`, `β`, `γ` with decidable equality on `γ`, for any binary function `f` from type `α` to `β` to `γ`, for any finite sets `s` and `t` of type `α` and `β` respectively, and for any property `p` on `γ`, the property `p` holds for all elements in the image of the binary function `f` applied to each pair of elements from `s` and `t` if and only if for all elements `x` in `s` and for all elements `y` in `t`, the property `p` holds for `f(x, y)`. In other words, checking a property on all elements of the image set obtained by applying a binary function on pair of elements from two finite sets is equivalent to checking the property on application of the binary function on all such pairs.
More concisely: For any binary function between two finite sets with decidable equality on the codomain and any property on the codomain, the property holds for all images of pairs in the sets if and only if it holds for the images of each pair in the sets separately.
|
Finset.biUnion_image_left
theorem Finset.biUnion_image_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
(s.biUnion fun a => Finset.image (f a) t) = Finset.image₂ f s t
The theorem `Finset.biUnion_image_left` states that for all types `α`, `β`, and `γ` with `γ` having a decidable equality and given a binary function `f : α → β → γ` and finite sets `s : Finset α` and `t : Finset β`, the bi-union over `s` of the image of function `f a` applied on `t` is equivalent to the image of the binary function `f` applied on sets `s` and `t`. Here, the image of a function refers to the set of output values the function takes when applied to every element of the input set. This theorem essentially equates a union operation followed by an image operation with the image operation of a binary function.
More concisely: For functions between decidably equal types, the image of the bi-union of two sets under a binary function is equivalent to the bi-union of the images of each set under that function.
|