Set.Nonempty.of_image2_right
theorem Set.Nonempty.of_image2_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β},
(Set.image2 f s t).Nonempty → t.Nonempty
The theorem `Set.Nonempty.of_image2_right` states that for all types `α`, `β`, and `γ` and for any binary function `f : α → β → γ` and sets `s : Set α` and `t : Set β`, if the image of the binary function `f` when applied to sets `s` and `t` is non-empty, then the set `t` is non-empty as well. In mathematical terms, this theorem asserts that if there exist elements in the image of the function `f(a, b)` for elements `a` in set `s` and `b` in set `t`, then there must exist some elements in set `t`.
More concisely: If the image of a binary function under sets is non-empty, then one of the sets is non-empty.
|
Set.image2_image_left
theorem Set.image2_image_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β} (f : γ → β → δ) (g : α → γ),
Set.image2 f (g '' s) t = Set.image2 (fun a b => f (g a) b) s t
The theorem `Set.image2_image_left` states that for any types `α`, `β`, `γ`, and `δ`, any sets `s` of `α` and `t` of `β`, any function `f` from `γ` to `β` to `δ`, and any function `g` from `α` to `γ`, the image of the binary function `f` on the image of `g` on `s` and `t` is the same as the image of the binary function where `f` is composed with `g` on `s` and `t`. In other words, applying `f` on the image of `g` on a set is the same as applying `f` composed with `g` directly on the set. This theorem essentially formalizes one aspect of the interchangeability of the order of operations in function application on sets.
More concisely: For any sets $S:\alpha$, $T:\beta$, functions $f:\gamma \to \delta$, $g:\alpha \to \gamma$, the image of $f$ on the image of $g$ applied to $S$ and $T$ equals the image of $f \circ g$ applied to $S$ and $T$.
|
Set.image_image2_distrib_left
theorem Set.image_image2_distrib_left :
∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ} {s : Set α}
{t : Set β} {g : γ → δ} {f' : α' → β → δ} {g' : α → α'},
(∀ (a : α) (b : β), g (f a b) = f' (g' a) b) → g '' Set.image2 f s t = Set.image2 f' (g' '' s) t
This theorem, `Set.image_image2_distrib_left`, states that for any two types `α` and `β`, and any functions `f : α → β → γ`, `g : γ → δ` and `f' : α' → β → δ` and `g' : α → α'`, if for every pair of elements `a` from `α` and `b` from `β`, the composition `g (f a b)` equals `f' (g' a) b`, then for any sets `s : Set α` and `t : Set β`, the image of the set `Set.image2 f s t` under the function `g` is equal to the image of the set `t` under the function `Set.image2 f' (g' '' s)`. This captures a commutativity property between function composition and set image operations.
More concisely: If for all `a` in `α` and `b` in `β`, `g (f a b) = f' (g' a) b`, then `Set.image2 f (Set.image s g) t = Set.image (Set.image2 f' (g' ''' s)) t`.
|
Mathlib.Data.Set.NAry._auxLemma.5
theorem Mathlib.Data.Set.NAry._auxLemma.5 :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α → β → γ) (s : Set α) (t : Set β),
Set.image2 f s t = Function.uncurry f '' s ×ˢ t
The theorem `Mathlib.Data.Set.NAry._auxLemma.5` states that for any types `α`, `β`, and `γ`, and any binary function `f` from `α` and `β` to `γ`, and any sets `s` of type `α` and `t` of type `β`, the image of the binary function `f` over the sets `s` and `t` (as defined by `Set.image2`) is equal to the set obtained by uncurrying the function `f` and applying it to the Cartesian product of sets `s` and `t`. In other words, it asserts that these two different ways of mapping a binary function over two sets produce the same result set.
More concisely: For any types `α`, `β`, `γ`, sets `s` of type `α`, `t` of type `β`, and binary function `f` from `α` to `β` to `γ`, `Set.image2 (f : α → β) s t = {x ∈ γ | ∃ (a ∈ s) ∃ (b ∈ t), f a b = x}`. (The set on the right-hand side is obtained by applying the uncurried function `fun x y => f x y` to the Cartesian product `s × t`.)
|
Set.image2_inter_union_subset_union
theorem Set.image2_inter_union_subset_union :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t t' : Set β},
Set.image2 f (s ∩ s') (t ∪ t') ⊆ Set.image2 f s t ∪ Set.image2 f s' t'
This theorem states that for any types α, β, γ, any binary function `f` from α and β to γ, and any sets `s`, `s'` of α and `t`, `t'` of β, the image of the function `f` over the intersection of `s` and `s'` and the union of `t` and `t'` is a subset of the union of the image of `f` over `s` and `t` and the image of `f` over `s'` and `t'`. In mathematical terms, for any sets $s, s' \subseteq \alpha$, $t, t' \subseteq \beta$, and function $f: \alpha \times \beta \mapsto \gamma$, it is true that $f[(s \cap s') \times (t \cup t')] \subseteq f[s \times t] \cup f[s' \times t']$.
More concisely: For any sets $s, s' \subseteq \alpha$, $t, t' \subseteq \beta$, and function $f: \alpha \times \beta \rightarrow \gamma$, $f[(s \cap s') \times (t \cup t')] \subseteq f[s \times t] \cup f[s' \times t']$.
|
Set.image2_inter_subset_right
theorem Set.image2_inter_subset_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t t' : Set β},
Set.image2 f s (t ∩ t') ⊆ Set.image2 f s t ∩ Set.image2 f s t'
This theorem, `Set.image2_inter_subset_right`, states that for any types `α`, `β`, and `γ` and for any binary function `f` from `α → β → γ` and sets `s` of type `α` and `t`, `t'` of type `β`, the image of function `f` applied to the set `s` and the intersection of `t` and `t'` is a subset of the intersection of the image of `f` applied to the set `s` and `t` and the image of `f` applied to the set `s` and `t'`. In mathematical terms, it can be expressed as $f(s, t \cap t') \subseteq f(s, t) \cap f(s, t')$.
More concisely: For any types `α`, `β`, and `γ`, and sets `s` of type `α` and `t`, `t'` of type `β`, the image of the binary function `f` from `α × β` to `γ` applied to the cartesian product of `s` and `t ∩ t'` is a subset of the image of `f` applied to the cartesian product of `s` and `t` and the image of `f` applied to the cartesian product of `s` and `t'`. In mathematical terms, $f(s \times (t \cap t')) \subseteq f(s \times t) \cap f(s \times t')$.
|
Set.image2_left_comm
theorem Set.image2_left_comm :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} {s : Set α} {t : Set β}
{u : Set γ} {f : α → δ → ε} {g : β → γ → δ} {f' : α → γ → δ'} {g' : β → δ' → ε},
(∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)) →
Set.image2 f s (Set.image2 g t u) = Set.image2 g' t (Set.image2 f' s u)
This theorem, `Set.image2_left_comm`, states that for any types `α`, `β`, `γ`, `δ`, `δ'`, `ε`, and three sets `s` of type `α`, `t` of type `β`, and `u` of type `γ`, given two binary functions `f : α → δ → ε`, `g : β → γ → δ`, a binary function `f' : α → γ → δ'`, and another binary function `g' : β → δ' → ε`, if for every element `a` in set `s`, `b` in set `t`, and `c` in set `u`, the result of applying `f` to `a` and the result of applying `g` to `b` and `c` equals the result of applying `g'` to `b` and the result of applying `f'` to `a` and `c`, then the image of set `s` under the binary function `f` and the image of the image of sets `t` and `u` under the binary function `g` is equal to the image of the image of sets `t` and `s` under the binary function `g'` and `f'` respectively. This is a form of left commutativity property in the context of set images under binary functions.
More concisely: For sets $s:\alpha$, $t:\beta$, $u:\gamma$, and functions $f:\alpha \rightarrow \delta \rightarrow \varepsilon$, $g:\beta \rightarrow \gamma \rightarrow \delta$, $f':\alpha \rightarrow \gamma \rightarrow \delta'$, and $g':\beta \rightarrow \delta' \rightarrow \varepsilon$, if $f(a, g(b, c)) = g'(b, f'(a, c))$ for all $a \in s$, $b \in t$, and $c \in u$, then $f[s] \subseteq g'[g[t], f'[s]]$.
|
Set.image2_image2_image2_comm
theorem Set.image2_image2_image2_comm :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {ε' : Type u_10} {ζ : Type u_11}
{ζ' : Type u_12} {ν : Type u_13} {s : Set α} {t : Set β} {u : Set γ} {v : Set δ} {f : ε → ζ → ν} {g : α → β → ε}
{h : γ → δ → ζ} {f' : ε' → ζ' → ν} {g' : α → γ → ε'} {h' : β → δ → ζ'},
(∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d)) →
Set.image2 f (Set.image2 g s t) (Set.image2 h u v) = Set.image2 f' (Set.image2 g' s u) (Set.image2 h' t v)
The theorem `Set.image2_image2_image2_comm` states that for all sets `s` of type `α`, `t` of type `β`, `u` of type `γ`, and `v` of type `δ`, and for all binary functions `f : ε → ζ → ν`, `g : α → β → ε`, `h : γ → δ → ζ`, `f' : ε' → ζ' → ν`, `g' : α → γ → ε'`, and `h' : β → δ → ζ'`, if for all elements `a` from `α`, `b` from `β`, `c` from `γ` and `d` from `δ`, the function `f` applied to the results of `g` applied to `a` and `b` and `h` applied to `c` and `d` equals `f'` applied to the results of `g'` applied to `a` and `c` and `h'` applied to `b` and `d`, then the image of `f` with respect to the image of `g` with sets `s` and `t` and the image of `h` with sets `u` and `v` equals the image of `f'` with respect to the image of `g'` with sets `s` and `u` and the image of `h'` with sets `t` and `v`. This theorem expresses a kind of commutativity property for the operation of forming images of binary functions applied to elements of sets.
More concisely: If for all `a: α, b: β, c: γ, d: δ, f, g, h, f', g', h', `image (f) (image (g) (s) × image (h) (u)) = image (f') (image (g') (s) × image (h') (t))`, then `image (f) (image (g) (s)) ⊆ image (f') (image (g') (s) × image (h') (t))` and `image (f') (image (g') (s) × image (h') (t)) ⊆ image (f) (image (g) (s))`.
|
Set.image2_right_identity
theorem Set.image2_right_identity :
∀ {α : Type u_1} {β : Type u_3} {f : α → β → α} {b : β},
(∀ (a : α), f a b = a) → ∀ (s : Set α), Set.image2 f s {b} = s
This theorem states that if `b` is a right identity for a binary function `f : α → β → α` (i.e., for every `a` of type `α`, `f a b` equals `a`), then the set containing only `b` is a right identity for the function `Set.image2 f`. In other words, for any set `s` of type `α`, the image of `s` and `{b}` under `f` is just `s` itself. This theorem generalizes the concept of a right identity from individual elements to sets of elements.
More concisely: If `b` is a right identity for a binary function `f : α → β → α`, then `Set.image2 f (s : set α) = s` for all sets `s`.
|
Set.image2_union_left
theorem Set.image2_union_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t : Set β},
Set.image2 f (s ∪ s') t = Set.image2 f s t ∪ Set.image2 f s' t
This theorem is about the image of a binary function with respect to set operations. Specifically, it states that for any types `α`, `β`, and `γ`, and any binary function `f` from `α` and `β` to `γ`, if `s` and `s'` are two subsets of `α` and `t` is a subset of `β`, then the image of the function `f` over the union of `s` and `s'` and `t` is equal to the union of the image of the function `f` over `s` and `t` and the image of the function `f` over `s'` and `t`. In mathematical terms, this can be written as `f((s ∪ s') × t) = f(s × t) ∪ f(s' × t)`.
More concisely: For any sets `A, B, C`, binary function `f : A × B → C`, and subsets `S, S' ⊆ A` and `T ⊆ B`, `f(S × T) = f(S × {}) ∪ f(S' × T)`. (Note: The empty set `{}` in the second term is implied by the context of sets `A` and `B`).
|
Set.image2_image_left_anticomm
theorem Set.image2_image_left_anticomm :
∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β}
{f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ},
(∀ (a : α) (b : β), f (g a) b = g' (f' b a)) → Set.image2 f (g '' s) t = g' '' Set.image2 f' t s
The theorem `Set.image2_image_left_anticomm` states that for any types `α`, `α'`, `β`, `γ`, and `δ`, any sets of `α` and `β` denoted by `s` and `t` respectively, 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 `γ`, provided that for all elements `a` in `α` and `b` in `β`, the function `f` applied to `g(a)` and `b` equals to the function `g'` applied to `f'(b,a)`, then the result of applying `Set.image2` on function `f` and the image of `s` under function `g` and set `t` equals the image of `Set.image2` on function `f'`, set `t`, and set `s` under function `g'`.
In plain language, this theorem establishes a certain condition under which the operation of forming the image of a pair of sets under a binary function commutes with the operation of first transforming one of the sets using a function and then forming the image under another binary function.
More concisely: If for all pairs of elements from types `α`, `β`, the function `f` applied to the image of an element under `g` and another element equals the image under `g'` of the function `f'` applied to those elements, then the image of the image of sets `s` and `t` under `g` and `f` equals the image of the image of sets `s` and `t` under `g'` and `f'`.
|
Set.image2_congr'
theorem Set.image2_congr' :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f f' : α → β → γ} {s : Set α} {t : Set β},
(∀ (a : α) (b : β), f a b = f' a b) → Set.image2 f s t = Set.image2 f' s t
The theorem `Set.image2_congr'` states that for any types `α`, `β`, and `γ` and for any two binary functions `f` and `f'` from `α` and `β` to `γ`, and any sets `s` of `α` and `t` of `β`, if `f` and `f'` produce the same result for all combinations of elements from `α` and `β`, then the image of `f` over `s` and `t` is the same as the image of `f'` over `s` and `t`. In mathematical terms, if `f(a, b) = f'(a, b)` for all `a` in `α` and `b` in `β`, then the set of all `c` where `c = f(a, b)` for some `a` in `s` and `b` in `t` is equal to the set of all `c` where `c = f'(a, b)` for the same `a` in `s` and `b` in `t`.
More concisely: If two functions from type `α × β` to type `γ` agree on all inputs from sets `s ∈ α` and `t ∈ β`, then their images over `s × t` are equal.
|
Set.image2_empty_left
theorem Set.image2_empty_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {t : Set β}, Set.image2 f ∅ t = ∅
This theorem states that for all types `α`, `β`, and `γ`, and for any binary function `f` from `α` and `β` to `γ`, and any set `t` of type `β`, the image of `f` when the first set is the empty set and the second set is `t`, is the empty set. In other words, when we take a binary function and apply it to pairs of elements where the first element is from an empty set, the result is always an empty set, regardless of what the second set is.
More concisely: For all types `α`, `β`, and `γ`, and for any binary function `f` from `α` to `β`, the image of `f` applied to the empty set is an empty set.
|
Set.image2_congr
theorem Set.image2_congr :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f f' : α → β → γ} {s : Set α} {t : Set β},
(∀ a ∈ s, ∀ b ∈ t, f a b = f' a b) → Set.image2 f s t = Set.image2 f' s t
This theorem, `Set.image2_congr`, states that for any given types `α`, `β`, and `γ`, and any two binary functions `f` and `f'` from `α` and `β` to `γ`, along with sets `s` of type `α` and `t` of type `β`, if for every element `a` of set `s` and every element `b` of set `t`, `f a b` is equal to `f' a b`, then the image of function `f` over sets `s` and `t` is equal to the image of function `f'` over the same sets. In mathematical terms, if two binary functions produce the same results for all possible combinations of elements of two sets, then their images over these sets are equal.
More concisely: If two binary functions from sets `α` and `β` to set `γ` agree on all elements of sets `s` and `t`, then the images of these functions over sets `s` and `t` are equal.
|
Set.image2_subset
theorem Set.image2_subset :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t t' : Set β},
s ⊆ s' → t ⊆ t' → Set.image2 f s t ⊆ Set.image2 f s' t'
This theorem asserts that the function `image2` is monotone with respect to the subset operation `⊆`. In other words, for any types `α`, `β`, and `γ`, and any binary function `f : α → β → γ`, if `s` is a subset of `s'` and `t` is a subset of `t'` (where `s` and `s'` are sets of `α`, and `t` and `t'` are sets of `β`), then the image of the binary function `f` applied to `s` and `t` is a subset of the image of the binary function `f` applied to `s'` and `t'`. In mathematical notation, this would be represented as: if $s \subseteq s'$ and $t \subseteq t'$, then $f(s,t) \subseteq f(s',t')$.
More concisely: For any functions $f : \alpha \to \beta \to \gamma$ and sets $s \subseteq s'$ of type $\alpha$ and $t \subseteq t'$ of type $\beta$, we have $f(s,t) \subseteq f(s',t')$.
|
Set.image2_union_right
theorem Set.image2_union_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t t' : Set β},
Set.image2 f s (t ∪ t') = Set.image2 f s t ∪ Set.image2 f s t'
The theorem `Set.image2_union_right` states that for any types `α`, `β`, and `γ`, any function `f` from `α` and `β` to `γ`, any set `s` of type `α`, and any two sets `t` and `t'` of type `β`, the image of the binary function `f` over the set `s` and the union of sets `t` and `t'` is equal to the union of the image of the binary function `f` over the set `s` and the set `t` and the image of the binary function `f` over the set `s` and the set `t'`. In mathematical notation, this can be written as: if `f: α × β → γ` and `s ⊆ α` and `t, t' ⊆ β`, then `f((s × (t ∪ t')) = f(s × t) ∪ f(s × t')`.
More concisely: For any functions `f: α × β → γ`, sets `s ⊆ α`, and sets `t, t' ⊆ β`, `f(s × (t ∪ t')) = f(s × t) ∪ f(s × t')`.
|
Set.image2_subset_right
theorem Set.image2_subset_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t : Set β},
s ⊆ s' → Set.image2 f s t ⊆ Set.image2 f s' t
The theorem `Set.image2_subset_right` states that for any types `α`, `β`, and `γ`, and a binary function `f` from `α` and `β` to `γ`, if a set `s` of type `α` is a subset of another set `s'` of type `α`, then the image of the function `f` when applied to the sets `s` and `t` (of type `β`) is a subset of the image of the function `f` when applied to the sets `s'` and `t`. In other words, this theorem enforces the property that the image of a smaller set under a function is a subset of the image of a larger set under the same function, when the function is applied to a fixed second set.
More concisely: For any functions $f : \alpha \times \beta \rightarrow \gamma$ and sets $s \subseteq s' \subseteq \alpha$, we have $f(s \times t) \subseteq f(s' \times t)$ for all $t \in \beta$.
|
Set.image2_inter_subset_left
theorem Set.image2_inter_subset_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t : Set β},
Set.image2 f (s ∩ s') t ⊆ Set.image2 f s t ∩ Set.image2 f s' t
The theorem `Set.image2_inter_subset_left` states that for all types `α`, `β`, and `γ`, and for all functions `f` from `α` and `β` to `γ`, if `s` and `s'` are sets of type `α` and `t` is a set of type `β`, then the image of the function `f` when applied on the intersection of the sets `s` and `s'` and the set `t` (expressed as `Set.image2 f (s ∩ s') t`) is a subset of the intersection of the image of the function `f` when applied on `s` and `t` and the image of `f` when applied on `s'` and `t` (expressed as `Set.image2 f s t ∩ Set.image2 f s' t`). In simpler terms, it asserts that the image of the intersection of two sets under a function is a subset of the intersection of the images of the individual sets under the same function.
More concisely: For all types `α`, `β`, and `γ`, and functions `f` from `α` to `γ`, if `s` and `s'` are sets of type `α`, then `Set.image2 f (s ∩ s')` is a subset of `Set.image2 f s ∩ Set.image2 f s'`.
|
Set.image2_mk_eq_prod
theorem Set.image2_mk_eq_prod :
∀ {α : Type u_1} {β : Type u_3} {s : Set α} {t : Set β}, Set.image2 Prod.mk s t = s ×ˢ t
This theorem states that for all types `α` and `β`, and for all sets `s` of type `α` and `t` of type `β`, the image of the binary function `Prod.mk` (which creates pairs `(a, b)` of elements `a` from `s` and `b` from `t`) is equal to the Cartesian product of the sets `s` and `t`. In other words, applying `Prod.mk` to each pair of elements from `s` and `t` produces exactly the same set as the Cartesian product of `s` and `t`.
More concisely: For all types `α` and `β`, and sets `s` of type `α` and `t` of type `β`, the set of pairs `{ Prod.mk a b | a ∈ s, b ∈ t }` is equal to the Cartesian product `s × t`.
|
Mathlib.Data.Set.NAry._auxLemma.6
theorem Mathlib.Data.Set.NAry._auxLemma.6 :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α → β → γ) {s : Set α} {t : Set β},
Set.image2 f s t = (fun x => f x.1 x.2) '' s ×ˢ t
The theorem `Mathlib.Data.Set.NAry._auxLemma.6` states that for any types `α`, `β`, and `γ`, and any binary function `f : α → β → γ`, the image of `f` over a set `s` of type `α` and a set `t` of type `β`, denoted as `Set.image2 f s t`, is equal to the set of all possible outputs of `f` when the input is a pair `(x.1, x.2)`, where `x` ranges over the Cartesian product of the sets `s` and `t`, denoted as `s ×ˢ t`. In mathematical notation, this is equivalent to saying that the image of `f` over `s ×ˢ t` is the set `{f(x, y) | (x, y) ∈ s × t }`.
More concisely: The theorem states that for any types `α`, `β`, and `γ`, and binary function `f : α → β → γ`, the set `Set.image2 f s t` equals the image of `f` over the Cartesian product `s ×ˢ t`, i.e., `{f(x, y) | (x, y) ∈ s × t}`.
|
Set.image_image2_right_anticomm
theorem Set.image_image2_right_anticomm :
∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β}
{f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ},
(∀ (a : α) (b : β), f a (g b) = g' (f' b a)) → Set.image2 f s (g '' t) = g' '' Set.image2 f' t s
The theorem `Set.image_image2_right_anticomm` asserts that for any types `α`, `β`, `β'`, `γ`, and `δ`, any sets `s` of `α` and `t` of `β`, 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 `γ`, if for every `α` and `β`, `f` of `α` and `g` of `β` equals `g'` of `f'` of `β` and `α`, then the image under `f` of set `s` and the image under `g` of set `t` is equal to the image under `g'` of the image under `f'` of set `t` and `s`. In more mathematical terms, if $f(\alpha, g(\beta)) = g'(f'(\beta, \alpha))$ for all $\alpha \in \text{Set } \alpha$ and $\beta \in \text{Set } \beta$, then the image of the binary function `f` on the set `s` and the image of the unary function `g` on the set `t` is equal to the image of the unary function `g'` on the image of the binary function `f'` on the set `t` and `s`.
More concisely: If for all $\alpha \in \alpha$ and $\beta \in \beta$, $f(\alpha, g(\beta)) = g'(f'(\beta, \alpha))$, then $f(s) \subseteq g'(f'(t \cup s))$. (This is a subset inclusion version of the theorem, assuming the functions preserve the set structures and the domains allow such operations.)
|
Set.image2_singleton_left
theorem Set.image2_singleton_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {t : Set β} {a : α}, Set.image2 f {a} t = f a '' t
This theorem states that for any types `α`, `β`, and `γ`, any binary function `f` from `α` and `β` to `γ`, any set `t` of type `β`, and any element `a` of type `α`, the image under `f` of the set consisting only of element `a` and the set `t` is equal to the set of the image of `t` under the function `f` when `a` is the first argument of `f`. In mathematical terms, for a function `f : α × β → γ`, the image of `f` over `a` singleton and `t` is the same as the image of `t` under the function `f(a, .)`.
More concisely: For any function $f : \alpha \times \beta \rightarrow \gamma$, any $a \in \alpha$, and any $t \subseteq \beta$, the image of the singleton set $\{a\} \times t$ under $f$ equals the image of $t$ under the function $f(a, \cdot)$.
|
Set.image_uncurry_prod
theorem Set.image_uncurry_prod :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α → β → γ) (s : Set α) (t : Set β),
Function.uncurry f '' s ×ˢ t = Set.image2 f s t
This theorem states that for any types `α`, `β`, and `γ`, and for any function `f` from `α` and `β` to `γ`, and for any sets `s` of type `α` and `t` of type `β`, the image of the uncurried version of function `f` applied to the Cartesian product of sets `s` and `t` is equal to the image of the binary function `f` applied to the sets `s` and `t`. In other words, it asserts the equality of two ways of creating a set of elements in `γ`: one way is by uncurrying the function `f` and then applying it to each pair of elements in the Cartesian product of `s` and `t`, and the other way is by directly applying the binary function `f` to each pair of elements, with the first element from `s` and the second from `t`.
More concisely: For any functions `f` from `α × β` to `γ`, sets `s` of type `α`, and `t` of type `β`, the image of `f` applied to the Cartesian product `s × t` is equal to the set of values obtained by applying `f` binary to each pair in `s × t`.
|
Set.image_image2
theorem Set.image_image2 :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β} (f : α → β → γ) (g : γ → δ),
g '' Set.image2 f s t = Set.image2 (fun a b => g (f a b)) s t
This theorem states that for any types `α`, `β`, `γ`, and `δ`, any sets `s` of type `α` and `t` of type `β`, any binary function `f` from `α` and `β` to `γ`, and any function `g` from `γ` to `δ`, the image under `g` of the image under `f` of `s` and `t` is equal to the image under the function that first applies `f` and then applies `g` of `s` and `t`. In other words, it asserts that the operation of taking images of sets under functions respects the composition of functions, which is a fundamental property in set theory and functional analysis.
More concisely: For any sets $s$ of type $\alpha$, $t$ of type $\beta$, binary function $f$ from $\alpha$ and $\beta$ to $\gamma$, and function $g$ from $\gamma$ to $\delta$, the image of $s$ and $t$ under $g \circ f$ is equal to the image of $s$ under $f$ and then $t$ under $g$.
|
Set.forall_image2_iff
theorem Set.forall_image2_iff :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {p : γ → Prop},
(∀ z ∈ Set.image2 f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)
This theorem `Set.forall_image2_iff` states that for any types `α`, `β`, and `γ`; for any binary function `f: α → β → γ`; for any sets `s: Set α`, `t: Set β`; and for any property `p: γ → Prop`, the property `p` holds for all elements in the image of the function `f` applied to sets `s` and `t` if and only if the property `p` holds for all possible results of the function `f` applied to any element from `s` and any element from `t`. In simple terms, if you apply `f` to every possible pair of elements from `s` and `t` and the property `p` holds for all these results, then `p` also holds for all elements in the set generated by applying `f` to the sets `s` and `t`.
More concisely: For any types α, β, γ, function f: α → β → γ, sets s: Set α, t: Set β, and property p: γ → Prop, the function image of p under f applied to sets s and t is equal to {x : γ | ∃ a: α, ∃ b: β, a ∈ s ∧ b ∈ t ∧ p(f a b)}.
|
Set.image2_swap
theorem Set.image2_swap :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α → β → γ) (s : Set α) (t : Set β),
Set.image2 f s t = Set.image2 (fun a b => f b a) t s
The theorem `Set.image2_swap` states that for all types `α`, `β`, and `γ`, and for any binary function `f` from `α` and `β` to `γ`, and any sets `s` of type `α` and `t` of type `β`, the image of the function `f` over the sets `s` and `t` is equal to the image of the function `f` with its arguments swapped, over the sets `t` and `s`. In mathematical terms, this theorem asserts the commutativity of the image of a function over two sets, swapping the order of sets and the function arguments does not change the resulting set.
More concisely: For any type `α`, `β`, `γ`, set `s` of type `α`, set `t` of type `β`, and binary function `f` from `α` to `β`, the image of `f` over `s` and `t` equals the image of `f` with arguments swapped over `t` and `s`. In symbols, `image (f : α → β) (s : set α) (t : set β) = image (f) (t : set β) (s : set α)`.
|
Set.image2_image_right
theorem Set.image2_image_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β} (f : α → γ → δ) (g : β → γ),
Set.image2 f s (g '' t) = Set.image2 (fun a b => f a (g b)) s t
The theorem `Set.image2_image_right` states that for all sets `s` of type `α` and `t` of type `β`, and for all functions `f : α → γ → δ` and `g : β → γ`, the image of the binary function `f` on the set `s` and the image of `g` on set `t` (`g '' t`) is equal to the image of the binary function `(fun a b => f a (g b))` on the sets `s` and `t`. In other words, it shows that applying the function `g` to the elements of `t` before or after forming the image under the binary function `f` does not change the resulting set.
More concisely: For all sets `s` of type `α`, `t` of type `β`, functions `f : α → γ → δ`, and `g : β → γ`, the images `f '' s` and `(g '' t) → δ` under the binary functions `f` and `(λ a b, f a (g b))` are equal.
|
Set.image2_subset_iff
theorem Set.image2_subset_iff :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {u : Set γ},
Set.image2 f s t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u
The theorem `Set.image2_subset_iff` states that for all types `α`, `β`, `γ`, a binary function `f : α → β → γ`, and sets `s : Set α`, `t : Set β`, and `u : Set γ`, the image of the function `f` applied to the elements of sets `s` and `t` is a subset of set `u` if and only if for every element `x` in set `s` and for every element `y` in set `t`, the result of the function `f` applied to `x` and `y` is an element of set `u`. In mathematical terms, this theorem states that the image of a binary function mapped across two sets is a subset of another set if and only if every possible output of the function on elements of the two sets is an element of the third set.
More concisely: For sets \(s : Set \alpha, t : Set \beta, u : Set \gamma, f : \alpha \rightarrow \beta \rightarrow \gamma\), \(f(s) \subseteq u\) if and only if for all \(x : \alpha \in s\) and \(y : \beta\), \(f(x, y) \in u\).
|
Set.image2_image_left_comm
theorem Set.image2_image_left_comm :
∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β}
{f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ},
(∀ (a : α) (b : β), f (g a) b = g' (f' a b)) → Set.image2 f (g '' s) t = g' '' Set.image2 f' s t
This theorem, named `Set.image2_image_left_comm`, relates to sets and function images in Lean 4. Given two types `α` and `β`, and sets `s : Set α` and `t : Set β`, it asserts the equality of the image of a binary function `f : α' → β → γ` applied to the image of a function `g : α → α'` acting on set `s` and set `t`, and the image of a function `g' : δ → γ` applied to the image of a binary function `f' : α → β → δ` acting on sets `s` and `t`, provided that for all elements `a` in set `α` and `b` in set `β`, the function `f` applied to `g a` and `b` equals `g'` applied to `f' a b`. Mathematically, this can be written as: if `∀ (a : α) (b : β), f (g a) b = g' (f' a b)`, then `Set.image2 f (g '' s) t = g' '' Set.image2 f' s t`.
More concisely: If for all `a` in `α` and `b` in `β`, `f (g a) b = g' (f' a b)`, then `Set.image2 f (g(s)) t = g' (Set.image2 f' s t)`. Here, `s` is a set of type `α`, `f : α' → β → γ`, `g : α → α'`, `f' : α → β → δ`, and `g' : δ → γ`.
|
Set.image2_distrib_subset_left
theorem Set.image2_distrib_subset_left :
∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {γ' : Type u_6} {δ : Type u_7} {ε : Type u_9}
{s : Set α} {t : Set β} {u : Set γ} {f : α → δ → ε} {g : β → γ → δ} {f₁ : α → β → β'} {f₂ : α → γ → γ'}
{g' : β' → γ' → ε},
(∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)) →
Set.image2 f s (Set.image2 g t u) ⊆ Set.image2 g' (Set.image2 f₁ s t) (Set.image2 f₂ s u)
This theorem establishes a rule about the manipulations of the image of multiple binary functions under certain conditions. Specifically, it states that for any sets `s`, `t`, and `u` and any binary functions `f`, `g`, `f₁`, `f₂`, and `g'`, if `f` applied to an element from `s` and the result of `g` applied to an element from `t` and `u` is equal to `g'` applied to `f₁` applied to an element from `s` and `t` and `f₂` applied to an element from `s` and `u`, then the image under `f` of `s` and the image under `g` of `t` and `u` is a subset of the image under `g'` of the image under `f₁` of `s` and `t` and the image under `f₂` of `s` and `u`. It should be noted that this subset relation does not necessarily hold in the reverse direction.
More concisely: If for all x in s, y in t, and z in u, g(y, z) = f₁(x, y) * f₂(x, z) implies im f(s) ⊆ im (g' ∘ (f₁ ∘ π₁ ∘ π₂)) (s × t × u), where π₁ and π₂ are the projections onto the first two coordinates.
|
Set.image_prod
theorem Set.image_prod :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α → β → γ) {s : Set α} {t : Set β},
(fun x => f x.1 x.2) '' s ×ˢ t = Set.image2 f s t
The theorem `Set.image_prod` states that for all types `α`, `β`, and `γ`, and for any binary function `f` from `α` and `β` to `γ`, the image of the function `f` when applied to the Cartesian product of two sets `s` and `t` (where `s` is a set of elements of type `α` and `t` is a set of elements of type `β`), is equal to the image of the function `f` when it's applied separately to each element of the sets `s` and `t`. In mathematical terms, for a function `f : α × β → γ`, the image of `f` over the Cartesian product of `s` and `t` is the same as the set of all `f(a, b)` where `a` is in `s` and `b` is in `t`.
More concisely: For any function `f : α × β → γ`, the image of `f` on the Cartesian product `s × t` is equal to the set of all `f(a, b)` where `a` is in `s` and `b` is in `t`.
|
Set.image2_empty_right
theorem Set.image2_empty_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α}, Set.image2 f s ∅ = ∅
This theorem states that for any set `s` of elements of type `α` and function `f` of type `α → β → γ`, the image of `f` with respect to `s` and an empty set of type `β` is an empty set of type `γ`. In other words, if the second set in the function `Set.image2` is empty, then the resultant set will also be empty, no matter what the first set or the binary function is. In mathematical terms, this is expressed as: if `s` is a set and `f` is a function from `α × β` to `γ`, then the image of `f` applied to `s` and an empty set is an empty set.
More concisely: For any set `s` and function `f`: if `s` is a set and `f` maps `α × β` to `γ`, then `Set.image2 s empty set` is an empty set.
|
Set.image2_singleton
theorem Set.image2_singleton :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {a : α} {b : β}, Set.image2 f {a} {b} = {f a b} := by
sorry
This theorem states that for any types `α`, `β`, and `γ`, and for any binary function `f : α → β → γ`, the image of the function `f` on the sets `{a}` and `{b}`, where `a` is an element of `α` and `b` is an element of `β`, results in the set `{f a b}`. Essentially, this means that when you apply the function `f` to a singleton set containing `a` and a singleton set containing `b`, you get a singleton set containing the result of `f(a, b)`.
More concisely: For any functions `f : α → β → γ` and `a : α`, `b : β`, the sets `{f a b}` and `{f x y | x ∈ {a}, y ∈ {b}}` are equal.
|
Set.image_image2_distrib_right
theorem Set.image_image2_distrib_right :
∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ} {s : Set α}
{t : Set β} {g : γ → δ} {f' : α → β' → δ} {g' : β → β'},
(∀ (a : α) (b : β), g (f a b) = f' a (g' b)) → g '' Set.image2 f s t = Set.image2 f' s (g' '' t)
The theorem `Set.image_image2_distrib_right` states that for all types `α`, `β`, `β'`, `γ`, and `δ`, and for all functions `f : α → β → γ`, `g : γ → δ`, `f' : α → β' → δ`, `g' : β → β'`, and sets `s : Set α` and `t : Set β`, if for every `a` in `α` and `b` in `β` the equation `g (f a b) = f' a (g' b)` holds, then the image of the function `g` on 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 `s` and the image of the function `g'` on the set `t`. In other words, this theorem is a statement about the distributivity of the image of a function over the image of a binary function.
More concisely: For functions `f : α → β → γ`, `g : γ → δ`, `f' : α → β' → δ`, and `g' : β → β'`, sets `s : Set α` and `t : Set β`, if `g (f a b) = f' a (g' b)` for all `a ∈ α` and `b ∈ β`, then `image g (image f s t) = image (f' o g') (s × t)`.
|
Set.image2_left_identity
theorem Set.image2_left_identity :
∀ {α : Type u_1} {β : Type u_3} {f : α → β → β} {a : α},
(∀ (b : β), f a b = b) → ∀ (t : Set β), Set.image2 f {a} t = t
This theorem asserts that if an element `a` of a type `α` is a left identity for a binary function `f : α → β → β` (that is, for any element `b` of type `β`, `f a b` equals `b`), then a set containing only this element `{a}` behaves as a left identity for the function `Set.image2 f`, which maps sets of `α` and `β` to sets of `β`. Specifically, for any set `t` of type `β`, `Set.image2 f {a} t` equals `t`. This implies that applying the function `f` with `a` as the left argument to any element of `t` leaves the element unchanged, hence `t` is left invariant by `Set.image2 f {a}`.
More concisely: If an element `a` of type `α` is a left identity for a binary function `f : α → β → β`, then the set `{a}` is a left identity for the function `Set.image2 f` on sets of type `α` and `β`, meaning `Set.image2 f {a} t = t` for any set `t` of type `β`.
|
Set.image_subset_image2_right
theorem Set.image_subset_image2_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {a : α},
a ∈ s → f a '' t ⊆ Set.image2 f s t
The theorem `Set.image_subset_image2_right` states that for all types `α`, `β`, and `γ`, and for any binary function `f` from `α` and `β` to `γ`, and for any sets `s` of type `α` and `t` of type `β`, and for any element `a` of type `α`, if `a` is an element of the set `s`, then the image of the function `f` applied to `a` and any element in set `t`, is a subset of the image of the binary function `f` applied to the sets `s` and `t`. In other words, for all elements `a` in `s`, the set of all `f(a, b)` where `b` is in `t` is included in the set of all `f(a', b')` where `a'` is in `s` and `b'` is in `t`.
More concisely: For all sets $S:\alpha$, $T:\beta$, $f:\alpha \times \beta \rightarrow \gamma$, and $a:S$, if $a \in S$ then $f(a, T) \subseteq f(S \times T)$, where $f(a, T) := \{f(a, b) \mid b \in T\}$ and $f(S \times T) := \{f(a, b) \mid a \in S, b \in T\}$.
|
Set.image2_distrib_subset_right
theorem Set.image2_distrib_subset_right :
∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9}
{s : Set α} {t : Set β} {u : Set γ} {f : δ → γ → ε} {g : α → β → δ} {f₁ : α → γ → α'} {f₂ : β → γ → β'}
{g' : α' → β' → ε},
(∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)) →
Set.image2 f (Set.image2 g s t) u ⊆ Set.image2 g' (Set.image2 f₁ s u) (Set.image2 f₂ t u)
The theorem `Set.image2_distrib_subset_right` states that for any sets `s`, `t`, and `u` of types `α`, `β`, and `γ` respectively, and any mappings `f : δ → γ → ε`, `g : α → β → δ`, `f₁ : α → γ → α'`, `f₂ : β → γ → β'` and `g' : α' → β' → ε`, such that for all elements `a` in `s`, `b` in `t`, and `c` in `u`, the function application `f (g a b) c` is equal to `g' (f₁ a c) (f₂ b c)`, the image of the function `f` over the image of the function `g` on the Cartesian product `s × t` and the set `u` is a subset of the image of the function `g'` over the image of function `f₁` on the Cartesian product `s × u` and the image of function `f₂` on the Cartesian product `t × u`.
Stated more simply, this theorem is about the conditions under which one can interchange two pairs of nested mappings applied over certain sets. The theorem does not hold in the opposite direction due to the presence of cross terms on the right-hand side.
More concisely: For sets `s`, `t`, `u` and mappings `f`, `g`, `f₁`, `f₂`, `g'`, if `f (g a b) c = g' (f₁ a c) (f₂ b c)` for all `a ∈ s`, `b ∈ t`, and `c ∈ u`, then `Set.image2 (g ∘ f) (s × t × u) ⊆ Set.image2 (g' ∘ f₁ ∘ f₂) (s × u × u)`.
|
Set.image2_singleton_right
theorem Set.image2_singleton_right :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {b : β},
Set.image2 f s {b} = (fun a => f a b) '' s
This theorem states that, for any types `α`, `β`, and `γ`, any binary function `f` from `α` and `β` to `γ`, any set `s` of type `α`, and any element `b` of type `β`, the image of the binary function `f` when applied to the set `s` and the singleton set containing `b` is the same as the image of the function that maps each element `a` of `s` to `f a b`. In mathematical terms, it's saying that the image under `f` of `s` and the singleton set `{b}` is the same as the image under the function `a ↦ f(a, b)` of `s`.
More concisely: For any functions $f : \alpha \times \beta \to \gamma$, sets $s \subseteq \alpha$, and elements $b \in \beta$, the set $f''(s \times \{b\}) = \{f(a, b) \mid a \in s\}$.
|
Set.image2_eq_empty_iff
theorem Set.image2_eq_empty_iff :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β},
Set.image2 f s t = ∅ ↔ s = ∅ ∨ t = ∅
The theorem `Set.image2_eq_empty_iff` states that for any types `α`, `β`, and `γ`, and for any binary function `f : α → β → γ` and sets `s : Set α` and `t : Set β`, the image of the function `f` over sets `s` and `t` (represented as `Set.image2 f s t`) is empty if and only if set `s` is empty or set `t` is empty. In other words, a function applied to two sets will produce an empty set if and only if at least one of the original sets is empty.
More concisely: For any functions \(f : \alpha \to \beta \to \gamma\) and sets \(s : \text{Set } \alpha\) and \(t : \text{Set } \beta\), \( \text{Set.image2 } f \ s \ t = \emptyset \iff s = \emptyset \lor t = \emptyset \).
|
Set.image2_right_comm
theorem Set.image2_right_comm :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {δ' : Type u_8} {ε : Type u_9} {s : Set α} {t : Set β}
{u : Set γ} {f : δ → γ → ε} {g : α → β → δ} {f' : α → γ → δ'} {g' : δ' → β → ε},
(∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b) →
Set.image2 f (Set.image2 g s t) u = Set.image2 g' (Set.image2 f' s u) t
This theorem, `Set.image2_right_comm`, states that for all sets `s` of type `α`, `t` of type `β`, and `u` of type `γ`, and for all binary functions `f : δ → γ → ε`, `g : α → β → δ`, `f' : α → γ → δ'`, and `g' : δ' → β → ε`, if for each element `a` of `α`, `b` of `β`, and `c` of `γ`, the function `f` applied to the result of function `g` applied to `a` and `b`, and `c` (i.e., `f (g a b) c`) equals the result of function `g'` applied to the result of function `f'` applied to `a` and `c`, and `b` (i.e., `g' (f' a c) b`), then the image of function `f` across the image of function `g` across sets `s` and `t`, and set `u` equals the image of function `g'` across the image of function `f'` across sets `s` and `u`, and set `t`. This theorem basically deals with the commutativity of two different composition of functions when mapped over sets.
More concisely: If for all `a : α`, `b : β`, and `c : γ`, `f (g a b) c = g' (f' a c) b`, then `(Set.image2 f (Set.image g s t)) = Set.image (g' . f') (Set.image f' s u) . t`.
|
Set.image_image2_distrib
theorem Set.image_image2_distrib :
∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ}
{s : Set α} {t : Set β} {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'},
(∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)) → g '' Set.image2 f s t = Set.image2 f' (g₁ '' s) (g₂ '' t)
This theorem is about the distribution of the image of a binary function over the image of two sets under two mapping functions. Specifically, for any types `α`, `α'`, `β`, `β'`, `γ`, and `δ`, and any binary function `f` from `α` and `β` to `γ`, sets `s` of `α` and `t` of `β`, another function `g` from `γ` to `δ`, a binary function `f'` from `α'` and `β'` to `δ`, and two functions `g₁` from `α` to `α'` and `g₂` from `β` to `β'`, if it holds for all `a` in `α` and `b` in `β` that `g(f(a, b)) = f'(g₁(a), g₂(b))`, then the image of the set resulting from applying `f` to the elements of `s` and `t` under `g` equals the set resulting from applying `f'` to the images of `s` under `g₁` and `t` under `g₂`. This theorem essentially states that the sequence of applying a binary function and then a function to elements of two sets is equivalent to applying the function to the images of the sets under two other functions, given that the binary functions and the functions are related in a certain way.
More concisely: If for all `a` in `α` and `b` in `β`, `g(f(a, b)) = f'(g₁(a), g₂(b))`, then `g(⋃(map f (s ∣∣ X) ⋃ map f (t ∣∣ X))) = ⋃(map f' (map g₁ (s ∣∣ X) ⋃ map g₂ (t ∣∣ X)))`, where `s` and `t` are sets of `α` and `β` respectively, `X` is a type, `f` is a binary function from `α` and `β` to `γ`, `g` is a function from `γ` to `δ`, `f'` is a binary function from `α'` and `β'` to `δ`, and `g₁` is a function from `α` to `α'` and `g₂` is a function from `β` to `β'`.
|
Set.Nonempty.image2
theorem Set.Nonempty.image2 :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β},
s.Nonempty → t.Nonempty → (Set.image2 f s t).Nonempty
This theorem states that for any types `α`, `β`, and `γ`, and a binary function `f` from `α` and `β` to `γ`, if `s` is a non-empty set of type `α` and `t` is a non-empty set of type `β`, then the image of `s` and `t` under the function `f` (i.e., `Set.image2 f s t`) is also a non-empty set. This image set is formed by applying `f` to each pair of elements where the first element is from `s` and the second element is from `t`, and collecting the results. Therefore, as long as `s` and `t` have at least one element each, there will always be at least one result in the image set.
More concisely: For any types `α`, `β`, and `γ`, and a binary function `f` from `α × β` to `γ`, the image of two non-empty sets `s ∈ Set α` and `t ∈ Set β` under `f` is a non-empty set. (Set.image2 preserves non- emptiness)
|
Set.image_image2_right_comm
theorem Set.image_image2_right_comm :
∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {s : Set α} {t : Set β}
{f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ},
(∀ (a : α) (b : β), f a (g b) = g' (f' a b)) → Set.image2 f s (g '' t) = g' '' Set.image2 f' s t
This theorem, `Set.image_image2_right_comm`, states that for all types `α`, `β`, `β'`, `γ`, and `δ`, and for all sets `s` of type `α` and `t` of type `β`, and for all functions `f` from `α` to `β'` to `γ`, `g` from `β` to `β'`, `f'` from `α` to `β` to `δ`, and `g'` from `δ` to `γ`, if for all `a` of type `α` and `b` of type `β`, the value of `f` at `a` and `g` at `b` equals the value of `g'` at `f'` at `a` and `b`, then the image under `f` of the set `s` and the image under `g` of the set `t` equals the image under `g'` of the image under `f'` of the sets `s` and `t`.
In other words, it's asserting a property about the composition of functions and the interaction between these functions and sets, which essentially says that we can swap the order of taking images under certain conditions.
More concisely: For sets `s` and `t`, and functions `f`, `g`, `f'`, and `g'` with the given conditions, `f(s) = g(t)` if and only if `g'(f'(s) = t)`.
|
Set.image2_union_inter_subset
theorem Set.image2_union_inter_subset :
∀ {α : Type u_1} {β : Type u_3} {f : α → α → β} {s t : Set α},
(∀ (a b : α), f a b = f b a) → Set.image2 f (s ∪ t) (s ∩ t) ⊆ Set.image2 f s t
This theorem states that for any fixed type `α`, any type `β`, a binary function `f : α → α → β` that is symmetric (i.e., `f a b = f b a` for all `a` and `b`), and any two sets `s` and `t` of type `α`, the image under `f` of the union of `s` and `t` and the intersection of `s` and `t` is a subset of the image under `f` of `s` and `t`. Said differently, the theorem states that for all `a` in `s ∪ t` and `b` in `s ∩ t`, `f(a, b)` is also an element of the set `{f(a', b') | a' ∈ s, b' ∈ t}`.
More concisely: For any symmetric binary function `f` and sets `s` and `t` of the same type `α`, `image f (s ∪ t)` is a subset of `image f s ∪ image f t`, and similarly for intersections.
|
Set.image_image2_antidistrib_right
theorem Set.image_image2_antidistrib_right :
∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ} {s : Set α}
{t : Set β} {g : γ → δ} {f' : β → α' → δ} {g' : α → α'},
(∀ (a : α) (b : β), g (f a b) = f' b (g' a)) → g '' Set.image2 f s t = Set.image2 f' t (g' '' s)
The `Set.image_image2_antidistrib_right` theorem states that for all types `α`, `α'`, `β`, `γ`, `δ`, a binary function `f : α → β → γ`, a set `s` of type `α`, a set `t` of type `β`, a function `g : γ → δ`, a binary function `f' : β → α' → δ`, and a function `g' : α → α'`, if for all elements `a` of type `α` and `b` of type `β` it holds that `g (f a b) = f' b (g' a)`, then applying function `g` to the image of the binary function `f` on sets `s` and `t` is equal to the image of the binary function `f'` on set `t` and the image of function `g'` on set `s`.
In mathematical terms, this is saying that if `g ∘ f = f' ∘ (g' × id)`, where `∘` denotes function composition and `id` is the identity function, then `g` applied to the image of `f` mapped over the Cartesian product of `s` and `t` equals the image of `f'` mapped over the Cartesian product of `t` and the image of `g'` on `s`.
More concisely: If for all `a` in `α` and `b` in `β`, `g (f a b) = f' b (g' a)`, then `g (⋃ i in s, ∀ j in t, f i j) = ⋃ j in t, ∀ i in s, f' j (g' i)`.
|
Set.image2_assoc
theorem Set.image2_assoc :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {ε' : Type u_10} {s : Set α}
{t : Set β} {u : Set γ} {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'},
(∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)) →
Set.image2 f (Set.image2 g s t) u = Set.image2 f' s (Set.image2 g' t u)
This theorem, `Set.image2_assoc`, is about the associativity of the image of binary functions over sets. Given sets `s`, `t`, and `u` of types `α`, `β`, and `γ` respectively, and binary functions `f : δ → γ → ε`, `g : α → β → δ`, `f' : α → ε' → ε`, and `g' : β → γ → ε'`, the theorem states that if for all elements `a` in `s`, `b` in `t`, and `c` in `u`, applying `f` to the result of `g a b` and `c` is equal to applying `f'` to `a` and the result of `g' b c`, then the image of `f` over the image of `g` over `s` and `t` and `u` is equal to the image of `f'` over `s` and the image of `g'` over `t` and `u`. In other words, changing the order of application of the binary functions and images doesn't change the final output set, provided the functions satisfy the stated condition.
More concisely: Given sets `s`, `t`, `u` and functions `f`, `g`, `f'`, `g'` as in the theorem statement, if for all `a in s`, `b in t`, and `c in u`, `f (g a b) c = f' a (g' b c)`, then `Set.image2 f (Set.image g s t) u` = `Set.image (f' . g') s t u`.
|
Set.Nonempty.of_image2_left
theorem Set.Nonempty.of_image2_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β},
(Set.image2 f s t).Nonempty → s.Nonempty
This theorem states that for any types `α`, `β`, and `γ`, and any binary function `f` from `α` and `β` to `γ`, if the image of `f` over sets `s` (of type `α`) and `t` (of type `β`) is not empty (i.e., there exists at least one element in `γ` that is the result of applying `f` to an element from `s` and an element from `t`), then set `s` itself must not be empty. In other words, if you can obtain at least one value by applying the function `f` to elements from sets `s` and `t`, then there must be at least one element in set `s`.
More concisely: If the image of a binary function from types `α` and `β` to `γ` is non-empty over sets `s` (of type `α`) and `t` (of type `β`), then `s` is non-empty.
|
Set.image_image2_antidistrib_left
theorem Set.image_image2_antidistrib_left :
∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ} {s : Set α}
{t : Set β} {g : γ → δ} {f' : β' → α → δ} {g' : β → β'},
(∀ (a : α) (b : β), g (f a b) = f' (g' b) a) → g '' Set.image2 f s t = Set.image2 f' (g' '' t) s
This theorem, `Set.image_image2_antidistrib_left`, establishes a relationship between image sets when applying transformations on the elements of the original sets. Specifically, it states that for every types `α`, `β`, `β'`, `γ`, `δ`, a binary function `f` from `α` and `β` to `γ`, a unary function `g` from `γ` to `δ`, a binary function `f'` from `β'` and `α` to `δ`, a unary function `g'` from `β` to `β'`, and sets `s` of `α` and `t` of `β`, if for every `a` in `α` and `b` in `β` the equality `g (f a b) = f' (g' b) a` holds, then the image of the set obtained by applying `f` to `s` and `t` under `g` is equal to the set obtained by applying `f'` to the image of `t` under `g'` and `s`.
In mathematical terms, given functions $f: \alpha \times \beta \rightarrow \gamma$, $g: \gamma \rightarrow \delta$, $f': \beta' \times \alpha \rightarrow \delta$, and $g': \beta \rightarrow \beta'$, and sets $s \subseteq \alpha$ and $t \subseteq \beta$, satisfying the condition $\forall a \in \alpha, b \in \beta, g(f(a, b)) = f'(g'(b), a)$, we have $g(f(s, t)) = f'(g'(t), s)$.
More concisely: If functions $f: \alpha \times \beta \to \gamma$, $g: \gamma \to \delta$, $f': \beta' \times \alpha \to \delta$, and $g': \beta \to \beta'$ satisfy $g(f(a, b)) = f'(g'(b), a)$ for all $a \in \alpha$ and $b \in \beta$, and $s \subseteq \alpha$ and $t \subseteq \beta$ are sets, then $g(f[s, t]) = f'[g'[t], s]$. (Here $[s, t]$ denotes the image of $s$ and $t$ under $f$.)
|
Mathlib.Data.Set.NAry._auxLemma.1
theorem Mathlib.Data.Set.NAry._auxLemma.1 :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {u : Set γ},
(Set.image2 f s t ⊆ u) = ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u
The theorem `Mathlib.Data.Set.NAry._auxLemma.1` states that for all types `α`, `β`, and `γ`, and a binary function `f : α → β → γ`, and sets `s : Set α`, `t : Set β`, and `u : Set γ`, the image of the function `f` on the sets `s` and `t` is a subset of `u` iff for any element `x` in `s` and any element `y` in `t`, the result of `f x y` is an element of `u`. In mathematical terms, the condition $(\forall x \in s, \forall y \in t, f(x, y) \in u)$ is equivalent to the statement that the image of the function `f` applied to elements of `s` and `t` is a subset of `u`.
More concisely: For sets $s$ of type $\alpha$, $t$ of type $\beta$, and $u$ of type $\gamma$, and a binary function $f : \alpha \times \beta \to \gamma$, the image of $f$ on $s$ and $t$ is a subset of $u$ if and only if for all $x \in s$ and $y \in t$, $f(x, y) \in u$.
|
Set.image2_union_inter_subset_union
theorem Set.image2_union_inter_subset_union :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t t' : Set β},
Set.image2 f (s ∪ s') (t ∩ t') ⊆ Set.image2 f s t ∪ Set.image2 f s' t'
This theorem states that for any types `α`, `β`, and `γ`, and any binary function `f : α → β → γ`, the image under `f` of the union of two sets `s` and `s'` in `α` and the intersection of two sets `t` and `t'` in `β` is a subset of the union of the images under `f` of `s` and `t` and `s'` and `t'`. In mathematical terms, this theorem is expressing the following subset relation: for any sets `s, s'` in `α` and `t, t'` in `β`, we have `f[(s ∪ s') × (t ∩ t')] ⊆ f[s × t] ∪ f[s' × t']`.
More concisely: For any types `α`, `β`, and `γ`, and any binary function `f : α → β → γ`, the image of the Cartesian product of the union of two sets in `α` and the intersection of two sets in `β` is a subset of the union of the images of each set in `α` and `β` under `f`. In symbols: `f[(s ∪ s') × (t ∩ t')] ⊆ f[s × t] ∪ f[s' × t']`, for any sets `s, s'` in `α` and `t, t'` in `β`.
|
Set.image2_subset_left
theorem Set.image2_subset_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t t' : Set β},
t ⊆ t' → Set.image2 f s t ⊆ Set.image2 f s t'
The theorem `Set.image2_subset_left` states that for any types `α`, `β`, and `γ`, and any function `f` from `α` and `β` to `γ`, if we have two sets `t` and `t'` of `β` such that `t` is a subset of `t'`, then the image of the binary function `f` when applied to any set `s` of `α` and the set `t` is also a subset of the image of the binary function `f` when applied to the same set `s` of `α` and the set `t'`. In other words, if we expand the set of second arguments to the function `f`, the set of output values will also expand accordingly.
More concisely: For any functions $f : \alpha \rightarrow \gamma$ and $s : \subset \alpha$, $t \subseteq t' \subseteq \beta$ imply $f(s \times t) \subseteq f(s \times t')$.
|
Set.image_image2_antidistrib
theorem Set.image_image2_antidistrib :
∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {f : α → β → γ}
{s : Set α} {t : Set β} {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'},
(∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)) → g '' Set.image2 f s t = Set.image2 f' (g₁ '' t) (g₂ '' s)
This theorem states that for any pair of sets `s` and `t` of types `α` and `β` respectively, any binary function `f` mapping elements of `α` and `β` to `γ`, and any functions `g` mapping `γ` to `δ`, `f'` mapping `β'` to `α'` and then to `δ`, and `g₁`, `g₂` mapping `β` to `β'` and `α` to `α'` respectively, such that for all elements `a` of `α` and `b` of `β`, `g (f a b)` equals `f' (g₁ b) (g₂ a)`, the image of the function `g` applied to the image of the binary function `f` applied to sets `s` and `t` is equal to the image of `f'` applied to the image of `g₁` applied to `t` and the image of `g₂` applied to `s`. In mathematical terms, it's about how the image of a function composition is related under certain conditions to the composition of the images of functions.
More concisely: For any sets `s` and `t`, functions `f: s × t -> γ`, `g: γ -> δ`, `f' : t -> s'`, `g₁: β -> β'`, and `g₂: α -> α'`, if for all `a in α` and `b in β`, `g (f a b) = f' (g₁ b) (g₂ a)`, then `g (∥f|_s×t⟩) = ∥f'_|_t⟩ (g₁) (g₂) (∥s⟩)`, where `∥_|_*⟩` denotes the image of a function applied to a set.
|
Set.image2_inter_union_subset
theorem Set.image2_inter_union_subset :
∀ {α : Type u_1} {β : Type u_3} {f : α → α → β} {s t : Set α},
(∀ (a b : α), f a b = f b a) → Set.image2 f (s ∩ t) (s ∪ t) ⊆ Set.image2 f s t
This theorem, `Set.image2_inter_union_subset`, states that for any two sets `s` and `t` of an arbitrary type `α`, and for any binary function `f : α → α → β` where `f` is commutative (i.e., `f a b = f b a` for any `a, b` in `α`), the image of the function `f` applied to the intersection of `s` and `t` and the union of `s` and `t` is a subset of the image of the function `f` applied to `s` and `t`. In mathematical notation, this is saying that if `f(a, b) = f(b, a)` for all `a, b` in `α`, then `f(s ∩ t, s ∪ t) ⊆ f(s, t)`.
More concisely: For commutative binary function `f` on type `α`, `f(s ∩ t, s ∪ t) ⊆ f(s, t)` holds for any sets `s` and `t` in `α`.
|
Set.image_subset_image2_left
theorem Set.image_subset_image2_left :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {b : β},
b ∈ t → (fun a => f a b) '' s ⊆ Set.image2 f s t
This theorem states that for any types `α`, `β`, and `γ`, any binary function `f` from `α` and `β` to `γ`, any sets `s` and `t` of `α` and `β` respectively, and any element `b` of `β`, if `b` is a member of `t`, then the image of the set `s` under the function `(fun a => f a b)` (which is a function from `α` to `γ` that takes an input from `s` and returns the output of `f` with that input and `b`) is a subset of the image of the binary function `f` applied to `s` and `t`. This means that applying `f` to each element of `s` paired with `b` results in a set of elements of `γ` that is entirely contained within the set of elements of `γ` obtained by applying `f` to each pair of elements from `s` and `t`.
More concisely: For any sets `S` in `α`, `T` in `β`, element `b` in `β`, and function `f` from `α` x `β` to `γ`, if `b` is in `T` then the image of `S` under the function `λx. f(x, b)` is a subset of the image of `f` applied to the Cartesian product `S` x `T`.
|
Set.image2_comm
theorem Set.image2_comm :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {g : β → α → γ},
(∀ (a : α) (b : β), f a b = g b a) → Set.image2 f s t = Set.image2 g t s
The `Set.image2_comm` theorem states that for any types `α`, `β`, and `γ`, any binary function `f` from `α` and `β` to `γ`, any set `s` of type `α`, any set `t` of type `β`, and any binary function `g` from `β` and `α` to `γ`, if for all `a` in `α` and `b` in `β` the result of `f` applied to `a` and `b` is equal to the result of `g` applied to `b` and `a`, then the image of `s` and `t` under `f` is equal to the image of `t` and `s` under `g`. In other words, if `f` and `g` are commutative with respect to their arguments, then the image of the sets under these functions are equal when the input sets are swapped.
More concisely: If functions `f : α × β → γ` and `g : β × α → γ` satisfy `f a b = g b a` for all `a : α` and `b : β`, then `Set.image2 f s t = Set.image2 g t s`.
|
Set.image2_nonempty_iff
theorem Set.image2_nonempty_iff :
∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β},
(Set.image2 f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
The theorem `Set.image2_nonempty_iff` states that for all types `α`, `β`, and `γ`, and for all functions `f` of type `α → β → γ`, and for sets `s` of type `Set α` and `t` of type `Set β`, the image of the function `f` over the sets `s` and `t` (denoted `Set.image2 f s t`) is nonempty if and only if both `s` and `t` are nonempty. In other words, you can only get elements in the image of `f` over `s` and `t` if both `s` and `t` have at least one element each.
More concisely: For functions between sets, the image of the function between two non-empty sets is a non-empty set.
|