Finset.map_eq_empty
theorem Finset.map_eq_empty : ∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α}, Finset.map f s = ∅ ↔ s = ∅
This theorem states that for any types `α` and `β`, for any embedding `f` from `α` to `β`, and for any finite set `s` of type `α`, the image of `s` under `f` is the empty set if and only if `s` itself is the empty set. In other words, an embedding `f` does not map any non-empty finite set to the empty set.
More concisely: For any types `α` and `β`, and any embedding `f` from `α` to `β`, if `s` is a finite non-empty set of type `α`, then `f(s)` is a non-empty set.
|
Finset.map_subtype_subset
theorem Finset.map_subtype_subset :
∀ {α : Type u_1} {t : Set α} (s : Finset ↑t), ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ t) s) ⊆ t := by
sorry
This theorem states that for any type `α` and a set `t` of this type, if we create a `Finset` from the subtype represented by `t`, and then map this `Finset` back to the main type `α` using `Function.Embedding.subtype`, the resulting `Finset` is a subset of the original set `t`. In other words, any elements we obtain by this process of subtyping and mapping back are guaranteed to belong to the original set `t`.
More concisely: For any type `α` and subtype `t` of `α`, the image of `t` under the embedding function to `Finset α` is a subset of `t`.
|
Mathlib.Data.Finset.Image._auxLemma.7
theorem Mathlib.Data.Finset.Image._auxLemma.7 :
∀ {α : Type u_1} {β : Type v} {f : α → β} {b : β} {s : Multiset α}, (b ∈ Multiset.map f s) = ∃ a ∈ s, f a = b := by
sorry
This theorem states that for any types `α` and `β`, any function `f` from `α` to `β`, any element `b` of type `β`, and any multiset `s` of type `α`, the statement "b is in the multiset obtained by mapping f over s" is equivalent to the existence of an element `a` in `s` such that `f(a)` equals `b`. In other words, an element `b` is in the multiset resulting from the map function if and only if there exists an element `a` in the original multiset `s` for which the function `f` maps `a` to `b`.
More concisely: For any functions $f:\alpha \to \beta$, elements $b \in \beta$, and multisets $s \subseteq \alpha$, $b$ is in the image multiset of $f$ over $s$ if and only if there exists an element $a \in s$ such that $f(a) = b$.
|
Mathlib.Data.Finset.Image._auxLemma.59
theorem Mathlib.Data.Finset.Image._auxLemma.59 :
∀ {n : ℕ} {s : Finset ℕ} (a : Fin n), (a ∈ Finset.fin n s) = (↑a ∈ s)
This theorem states that for any natural number `n`, any finite set `s` of natural numbers, and any natural number `a` less than `n`, `a` is an element of the set obtained by taking all elements of `s` that are less than `n` if and only if the natural number corresponding to `a` is an element of `s`. In other words, the operation of getting all elements of `s` less than `n` preserves membership: an element belongs to the resultant set if and only if it belongs to the original set.
More concisely: For any natural number `n`, set `s` of natural numbers, and natural number `a` less than `n`, `a` is an element of the set of natural numbers in `s` less than `n` if and only if `a` is an element of `s`.
|
Finset.image_inter_subset
theorem Finset.image_inter_subset :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : DecidableEq α] (f : α → β) (s t : Finset α),
Finset.image f (s ∩ t) ⊆ Finset.image f s ∩ Finset.image f t
This theorem states that for any two finite sets `s` and `t` of elements of some type `α`, and a function `f` from `α` to another type `β` (both `α` and `β` equipped with a decidable equality relation), the image of the intersection of `s` and `t` under `f` is a subset of the intersection of the images of `s` and `t` under `f`. In other words, if you apply the function `f` to each element in the intersection of `s` and `t`, every resulting value will also be in the intersection of the set obtained by applying `f` to `s` and the set obtained by applying `f` to `t`.
More concisely: For finite sets `s` and `t` of elements from a type `α` with decidable equality, and a function `f` from `α` to another type `β`, the image of `s ∩ t` under `f` is a subset of `f(s) ∩ f(t)`.
|
Finset.coe_map
theorem Finset.coe_map : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α), ↑(Finset.map f s) = ⇑f '' ↑s := by
sorry
This theorem states that for any embedding `f` from a type `α` to a type `β`, and for any finset `s` of type `α`, the set representation (coe) of the mapped finset (`Finset.map f s`) is equal to the image of the set representation of `s` under `f`. In other words, if we apply the embedding to each element of the finset and form a new finset from the results, converting this new finset into a set yields the same result as first converting the original finset into a set and then applying the embedding to each element.
More concisely: For any embedding `f` and finset `s`, the image of the set representation of `s` under `f` is equal to the set representation of the mapped finset `Finset.map f s`.
|
Mathlib.Data.Finset.Image._auxLemma.1
theorem Mathlib.Data.Finset.Image._auxLemma.1 :
∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {b : β}, (b ∈ Finset.map f s) = ∃ a ∈ s, f a = b := by
sorry
This theorem states that for all types α and β, for any embedding `f` from α to β, for any finite set `s` of type α, and for any element `b` of type β, `b` is in the image of `s` under `f` if and only if there exists an element `a` in `s` such that `f a` equals `b`. In other words, an element is in the image of a set under a function if and only if it is the image of some element from the original set under the function.
More concisely: For any functions between types and any sets and elements, an element is in the image of the set under the function if and only if there exists an element from the set whose image under the function is that element.
|
Finset.image_nonempty
theorem Finset.image_nonempty :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α},
(Finset.image f s).Nonempty ↔ s.Nonempty
This theorem, `Finset.image_nonempty`, states for any two types `α` and `β` with a decidable equality on `β`, any function `f` from `α` to `β`, and any finite set `s` of type `α`, the forward image of `s` under `f` (represented by `Finset.image f s`) is nonempty if and only if `s` itself is nonempty. In other words, a finite set `s` has a nonempty image under a function `f` precisely when `s` is not empty.
More concisely: For any decidably equalizable types `α` and `β`, function `f` from `α` to `β`, and finite set `s` of type `α`, the image `Finset.image f s` is nonempty if and only if `s` is nonempty.
|
Finset.image_union
theorem Finset.image_union :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : DecidableEq α] {f : α → β} (s₁ s₂ : Finset α),
Finset.image f (s₁ ∪ s₂) = Finset.image f s₁ ∪ Finset.image f s₂
The `Finset.image_union` theorem states that for all types `α` and `β`, given the condition that `β` has decidable equality and `α` has decidable equality, and given a function `f` from `α` to `β` and two finite sets `s₁` and `s₂` of type `α`, the forward image under `f` of the union of `s₁` and `s₂` is equal to the union of the forward images of `s₁` and `s₂` under `f`. This theorem basically asserts the preservation of set union under the image of a function, which is a fundamental property in set theory.
More concisely: For functions between type `α` and `β` with decidable equality, the image under `f` of the union of two finite sets `s₁` and `s₂` in `α` equals the union of the images of `s₁` and `s₂` under `f`.
|
Finset.Nonempty.image
theorem Finset.Nonempty.image :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {s : Finset α},
s.Nonempty → ∀ (f : α → β), (Finset.image f s).Nonempty
The theorem `Finset.Nonempty.image` states that for any types `α` and `β` where `β` has decidable equality, and for any nonempty finite set `s` of type `α`, the image of `s` under any function `f` from `α` to `β` is also nonempty. In other words, if we have a function `f` that maps elements from type `α` to type `β` and a nonempty finite set of elements of type `α`, then the set of images of these elements (obtained by applying function `f`) in `β` will also be nonempty.
More concisely: For any nonempty finite set `s` of type `α` and any function `f` from `α` to a type `β` with decidable equality, the image `f''s` is a nonempty set.
|
Finset.map_refl
theorem Finset.map_refl : ∀ {α : Type u_1} {s : Finset α}, Finset.map (Function.Embedding.refl α) s = s
The theorem `Finset.map_refl` states that for any type `α` and for any finite set `s` of type `α`, mapping `s` with the identity function, which is an embedding from `α` to `α`, will return `s` itself. In other words, applying the identity function to each element of the finite set doesn't change the set.
More concisely: For any finite set `s` of type `α`, the application of the identity function `id : α → α` to every element of `s` results in `s` itself, i.e., `id '' s = s`.
|
Mathlib.Data.Finset.Image._auxLemma.55
theorem Mathlib.Data.Finset.Image._auxLemma.55 :
∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α} {a : Subtype p},
(a ∈ Finset.subtype p s) = (↑a ∈ s)
This theorem states that for any type `α`, any decidable predicate `p` on `α`, any finite set `s` of `α`, and any element `a` of the subtype `p`, `a` belongs to the set obtained by applying the `Finset.subtype` function to `s` if and only if the element that `a` corresponds to in the type `α` belongs to `s`. In other words, an element from the subtype of `α` defined by `p` is in the subset of `s` consisting of elements satisfying `p` if and only if the original element in `α` is in `s`.
This theorem connects the membership relations in the original set and the subset formed by applying a decidable predicate, making it easier to deal with subsets that are defined by certain properties in the context of finite sets.
More concisely: For any type `α`, decidable predicate `p` on `α`, finite set `s` of `α`, and `a` in the subtype `p α`, `a` is in the subset `Finset.subtype s` if and only if the element `α` corresponding to `a` is in `s`.
|
Finset.image_insert
theorem Finset.image_insert :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : DecidableEq α] (f : α → β) (a : α) (s : Finset α),
Finset.image f (insert a s) = insert (f a) (Finset.image f s)
The theorem `Finset.image_insert` states that for any types `α` and `β`, given a function `f` from `α` to `β`, an element `a` of type `α`, and a finite set `s` of type `α`, the image of the function `f` applied to the set resulting from inserting `a` into `s` is equal to inserting the image of `a` under `f` into the image of `s` under `f`. In other words, we can either insert an element into a set and then take the image under a function, or we can take the image of the set and the element separately and then insert. This holds if the equality on `α` and `β` is decidable.
More concisely: For any decidably-equaled types `α` and `β`, given a function `f : α -> β` and a finite set `s : Finset α`, the application of `f` to the set `insert a s` is equal to the set `insert (f a) (map f s)`.
|
Finset.Nonempty.map
theorem Finset.Nonempty.map :
∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α}, s.Nonempty → (Finset.map f s).Nonempty
This theorem, referred to as "Alias of the reverse direction of `Finset.map_nonempty`", states that for any types `α` and `β`, and for any function `f` that is an embedding from `α` to `β`, if a `Finset` `s` of type `α` is non-empty, then the mapped `Finset` that is obtained by applying the function `f` to each element of `s` is also non-empty. In other words, the non-emptiness property is preserved under the operation of `Finset.map`.
More concisely: If `f` is an embedding from `α` to `β` and `s` is a non-empty `Finset` of type `α`, then `Finset.map f s` is a non-empty `Finset` of type `β`.
|
Finset.map_singleton
theorem Finset.map_singleton : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (a : α), Finset.map f {a} = {f a}
The theorem `Finset.map_singleton` states that for any types `α` and `β`, for any embedding function `f` from `α` to `β`, and for any element `a` in `α`, the image finset of a singleton finset containing the element `a` under the function `f` is a singleton finset containing the image of `a` under `f`. In more mathematical terms, if we map a singleton set `{a}` in `α` via an embedding `f`, we will get a singleton set `{f(a)}` in `β`.
More concisely: For any embedding function `f` and any element `a`, the image of the singleton finset `{a}` under `f` is the singleton finset `{f(a)}`.
|
Finset.map_map
theorem Finset.map_map :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ↪ β) (g : β ↪ γ) (s : Finset α),
Finset.map g (Finset.map f s) = Finset.map (f.trans g) s
The theorem `Finset.map_map` states that for all types `α`, `β`, and `γ`, with `f` being an embedding from `α` to `β`, `g` being an embedding from `β` to `γ`, and `s` being a finite set in `α`, mapping `s` through `f` and then `g` is equivalent to directly mapping `s` through the composition of `f` and `g`. In other words, the operation of mapping a finite set through two embeddings is associative.
More concisely: For all finite sets $s : \text{Finset} \ algebra_, \ f : \alpha \rightarrow \beta \ (\text{an embedding}), \ g : \beta \rightarrow \gamma \ (\text{an embedding}), \ \text{we have} \ \text{map} \ (f \circ g) \ s = \text{map} \ g \ (\text{map} \ f \ s)$.
|
Finset.map_injective
theorem Finset.map_injective : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β), Function.Injective (Finset.map f) := by
sorry
The theorem `Finset.map_injective` states that for all types `α` and `β`, if we have an embedding function `f` from `α` to `β`, then the operation of mapping a finset from `α` to `β` using this function is injective. In other words, if two finsets from `α` are mapped to the same finset in `β` using the function `f`, then these two finsets must have been the same to begin with. This theorem ensures that no information is lost when we map finsets from one type to another using an embedding function.
More concisely: If `f : α → β` is an embedding and `s1, s2 : Finset α`, then `Finset.map f s1 = Finset.map f s2` implies `s1 = s2`.
|
Mathlib.Data.Finset.Image._auxLemma.42
theorem Mathlib.Data.Finset.Image._auxLemma.42 : ∀ {α : Type u_1} {a b : α}, (b ∈ {a}) = (b = a)
This theorem, `Mathlib.Data.Finset.Image._auxLemma.42`, states that for all types `α` and for all elements `a` and `b` of that type, `b` is an element of the singleton set `{a}` if and only if `b` is equal to `a`. In other words, in the context of sets, an element `b` belongs to a set that only contains `a` if `b` is identical to `a`.
More concisely: For any type `α` and elements `a, b` of `α`, `b` is in the singleton set `{a}` if and only if `a = b`.
|
Finset.map_symm_subset
theorem Finset.map_symm_subset :
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {f : α ≃ β},
Finset.map f.symm.toEmbedding t ⊆ s ↔ t ⊆ Finset.map f.toEmbedding s
This theorem, `Finset.map_symm_subset`, establishes a relationship between two finsets `s` and `t` of types `α` and `β` respectively, and a bijective function `f` from `α` to `β`. Specifically, it states that the image of `t` under the function `f.symm.toEmbedding` being a subset of `s` is equivalent to `t` being a subset of the image of `s` under the function `f.toEmbedding`. In other words, it translates the concept of subset relationships between the original sets and their images under a function and its inverse.
More concisely: For finsets `s` of type `α` and `t` of type `β`, and a bijective function `f` from `α` to `β`, the sets `f.symm.toEmbedding '' t` and `s >>> f.toEmbedding` are equal if and only if `t` is a subset of `s`.
|
Mathlib.Data.Finset.Image._auxLemma.4
theorem Mathlib.Data.Finset.Image._auxLemma.4 : ∀ {α : Type u_1} {a : α} {s : Finset α}, (a ∈ ↑s) = (a ∈ s)
This theorem, `Mathlib.Data.Finset.Image._auxLemma.4`, states that for all types `α`, all elements `a` of type `α`, and all finite sets `s` of type `α`, the statement 'element `a` is in the coercive version of the set `s`' is equivalent to the statement 'element `a` is in the original set `s`'. In other words, coercing a finite set doesn't change whether an element is in that set.
More concisely: For all types `α`, elements `a` of `α`, and finite sets `s` of `α`, the element `a` is in the coercive version of `s` if and only if it is in `s`.
|
Finset.image_subset_image
theorem Finset.image_subset_image :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s₁ s₂ : Finset α},
s₁ ⊆ s₂ → Finset.image f s₁ ⊆ Finset.image f s₂
This theorem, named `Finset.image_subset_image`, states that for any two finite sets `s₁` and `s₂` of some type `α`, if `s₁` is a subset of `s₂`, then the image of `s₁` under a function `f` from `α` to some type `β` is a subset of the image of `s₂` under the same function `f`. Here, the equality of elements in type `β` is decidable. The image of a set under a function refers to the set of all the function's outputs when applied to each element of the original set. This theorem thus generalizes the property of subset relation preservation under function mapping.
More concisely: If `s₁` is a subset of `s₂` and `f` is a function, then `f(s₁)` is a subset of `f(s₂)`.
|
Finset.map_perm
theorem Finset.map_perm :
∀ {α : Type u_1} {s : Finset α} {σ : Equiv.Perm α}, {a | σ a ≠ a} ⊆ ↑s → Finset.map (Equiv.toEmbedding σ) s = s
This theorem states that for any type `α`, a finite set `s` of `α`, and a permutation `σ` of `α`, if the only elements that are not left fixed by `σ` are contained within `s`, then applying the permutation `σ` to `s` does not change `s`. In other words, if `σ` only permutes elements within `s` and leaves all other elements of `α` fixed, then the image of `s` under `σ` (denoted by `Finset.map (Equiv.toEmbedding σ) s`) is the same as `s` itself. The operation `Finset.map (Equiv.toEmbedding σ)` represents the action of applying the permutation `σ` to each element of the set `s`.
More concisely: If a permutation fixes all elements outside a finite set and only permutes elements within it, then the set is invariant under the permutation.
|
Mathlib.Data.Finset.Image._auxLemma.17
theorem Mathlib.Data.Finset.Image._auxLemma.17 : ∀ {a b c : Prop}, (a ∧ b → c) = (a → b → c)
This theorem, named as `Mathlib.Data.Finset.Image._auxLemma.17`, states that for any three propositions `a`, `b`, and `c`, the statement "`a` and `b` imply `c`" is equivalent to the statement "`a` implies that `b` implies `c`". In other words, if `a` and `b` are true, then `c` must be true is the same as saying that if `a` is true, then if `b` is also true, `c` must be true. This is a fundamental concept in propositional logic.
More concisely: The theorem `Mathlib.Data.Finset.Image._auxLemma.17` in Lean 4 states that the implication "`a` implies `b` implies `c`" is logically equivalent to "`a` and `b` imply `c`".
|
Finset.Nonempty.of_image
theorem Finset.Nonempty.of_image :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α},
(Finset.image f s).Nonempty → s.Nonempty
This theorem, referred to as an alias of the forward direction of `Finset.image_nonempty`, asserts that for any two types `α` and `β`, given a function `f` from `α` to `β` and a finite set `s` of type `α`, if the forward image of `s` under `f` is nonempty, then `s` is nonempty. In other words, if the set formed by applying `f` to each element of `s` has at least one element, then `s` must also have at least one element. The equality of elements in type `β` is assumed to be decidable.
More concisely: If `f` is a function from a non-empty type `α` to a type `β` and the image of a finite set `s` under `f` is nonempty, then `s` is nonempty.
|
Finset.filter_image
theorem Finset.filter_image :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {p : β → Prop}
[inst_1 : DecidablePred p],
Finset.filter p (Finset.image f s) = Finset.image f (Finset.filter (fun a => p (f a)) s)
The theorem `Finset.filter_image` states that for any types `α` and `β`, where `β` has decidable equality, and any function `f` from `α` to `β`, a `Finset` `s` of `α`, and a predicate `p` on `β` that is decidable, filtering with `p` on the forward image of `s` under `f` is equal to the forward image under `f` of the filter of `s` based on the predicate `(fun a => p (f a))`. In other words, the order of filtering and applying the function doesn't matter, you can first filter the elements according to the predicate and then apply the function, or first apply the function and then filter the results.
More concisely: For any type `α`, type `β` with decidable equality, function `f` from `α` to `β`, decidable predicate `p` on `β`, and `Finset` `s` of `α`, the filtered images of `s` under `f` and `p` commute: `(filter p (map f s)) = (map f (filter (λ a, p (f a)) s))`.
|
Finset.image_symmDiff
theorem Finset.image_symmDiff :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : DecidableEq α] {f : α → β} (s t : Finset α),
Function.Injective f → Finset.image f (symmDiff s t) = symmDiff (Finset.image f s) (Finset.image f t)
This theorem states that for any two finite sets `s` and `t` of elements of type `α` and any injective function `f` from `α` to `β`, where `β` has decidable equality, the image of the symmetric difference of `s` and `t` under `f` is equal to the symmetric difference of the images of `s` and `t` under `f`. In other words, an injective function preserves the symmetric difference operation under the mapping from one finite set to another.
More concisely: For injective functions `f` from finite sets `s` and `t` of type `α` to type `β` with decidable equality, `f(s ⊖ t) = f(s) ⊖ f(t)`.
|
Finset.attach_image_val
theorem Finset.attach_image_val :
∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α}, Finset.image Subtype.val s.attach = s
This theorem states that for any given type `α` with decidable equality and any finite set `s` of type `α`, the image of the attached set of `s` under the value function `Subtype.val` is equal to the original set `s`. In more layman's terms, when we attach each element of a finite set to the property of being in that set, creating a new set of subtypes, and then apply a function that retrieves the original element from each subtype, we get back the original set.
More concisely: For any finite type `α` with decidable equality, the image of a set `s` under the `Subtype.val` function is equal to `s` itself.
|
Finset.image_id'
theorem Finset.image_id' : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α], Finset.image (fun x => x) s = s := by
sorry
The theorem `Finset.image_id'` states that for all types `α` and all finite sets `s` of this type, assuming `α` has decidable equality, the image of the set `s` under the identity function (i.e., each element of the set is mapped to itself) is equal to the original set `s`. This essentially means applying the identity function to a finite set does not change the set.
More concisely: For any type `α` with decidable equality and finite set `s` of `α`, the image of `s` under the identity function is equal to `s`.
|
Finset.image_toFinset
theorem Finset.image_toFinset :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} [inst_1 : DecidableEq α] {s : Multiset α},
Finset.image f s.toFinset = (Multiset.map f s).toFinset
This theorem states that for any two types `α` and `β` where `β` has a decidable equality, for any function `f` from `α` to `β`, and for any equation with decidable equality in `α`, if you apply the function `f` to a multiset `s` of type `α`, convert it to a finiset and then take the image under `f`, it is equal to mapping the function `f` to the multiset `s` first and then converting it to a finiset. In other words, the order of operations - finiset conversion and image under a function - does not matter.
More concisely: For any functions `f: α → β` with decidable equality and decidable types `α` and `β`, the application of `f` to a multiset `s` of type `α`, conversion to a finiset, and taking the image under `f` is equal to first mapping `f` to `s` and then converting the resulting multiset to a finiset.
|
Finset.image_comm
theorem Finset.image_comm :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq β] {s : Finset α} {β' : Type u_4}
[inst_1 : DecidableEq β'] [inst_2 : DecidableEq γ] {f : β → γ} {g : α → β} {f' : α → β'} {g' : β' → γ},
(∀ (a : α), f (g a) = g' (f' a)) → Finset.image f (Finset.image g s) = Finset.image g' (Finset.image f' s)
The theorem `Finset.image_comm` states that for any types `α`, `β`, `γ`, and `β'` and any finite set `s` of type `α`, if we have two functions `f : β → γ`, `g : α → β`, another function `f' : α → β'` and `g' : β' → γ`, where `β`, `β'` and `γ` are types with decidable equality, then if for every element `a` of type `α`, `f(g(a))` is equal to `g'(f'(a))`, the image of the image of `s` under `g` then `f` is the same as the image of the image of `s` under `f'` then `g'`. In other words, the order of composition of these two pairs of functions in the image operation does not matter as long as the functions satisfy the said property.
More concisely: If `f : β → γ`, `g : α → β`, `f' : α → β'`, `g' : β' → γ` are functions with decidable equality types `β`, `β'`, and `γ`, and `s` is a finite set of type `α`, then `g''(f(x)) = f'(g(x))` for all `x` in `s` implies `f(g(s)) = g'(f'(s))`.
|
Finset.image_image
theorem Finset.image_image :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq β] {f : α → β} {s : Finset α}
[inst_1 : DecidableEq γ] {g : β → γ}, Finset.image g (Finset.image f s) = Finset.image (g ∘ f) s
The `Finset.image_image` theorem states that for all sets `s` of type `α`, functions `f : α → β` and `g : β → γ`, and given that the equality of elements in `β` and `γ` are decidable, then the image of the set `s` under `f` followed by the image under `g` is the same as the image of the set `s` under the composition of `g` and `f`. In other words, applying `g` to the image of `s` under `f` is the same as applying the composition of `g` and `f` to `s`. This theorem formalizes the concept of the composition of functions in the context of the images of finite sets.
More concisely: For any decidably equal sets `β` and sets `s` of type `α`, the image of `s` under the composition of functions `g : β → γ` and `f : α → β` is equal to the image of `s` under `g` followed by the image under `f`.
|
Finset.image_id
theorem Finset.image_id : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α], Finset.image id s = s
This theorem, `Finset.image_id`, states that for any type `α` with decidable equality and any finite set `s` of type `α`, the image of `s` under the identity function is identical to `s` itself. In other words, if we apply the identity function to each element of the finite set `s`, the resulting set is exactly `s`. This is analogous to the mathematical property that the image of a set under the identity map is the set itself.
More concisely: For any finite set `s` of type `α` with decidable equality, the image of `s` under the identity function is equal to `s`.
|
Mathlib.Data.Finset.Image._auxLemma.2
theorem Mathlib.Data.Finset.Image._auxLemma.2 :
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α ≃ β} {b : β},
(b ∈ Finset.map f.toEmbedding s) = (f.symm b ∈ s)
This theorem states that for any types `α` and `β`, any finset `s` of type `α`, an equivalence relation `f` from `α` to `β`, and any element `b` of type `β`, the element `b` belongs to the image of the finset `s` under the mapping `f` if and only if the inverse image of `b` under `f` belongs to the finset `s`. In other words, it states that the image of a finset under an equivalence relation contains a particular element if and only if the original finset contains the preimage of that element.
More concisely: For any equivalence relation f between types α and β, finset s ∈ α, and b ∈ β, the element b is in the image of s under f if and only if the inverse image of b under f is in s.
|
Finset.image_singleton
theorem Finset.image_singleton :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α → β) (a : α), Finset.image f {a} = {f a}
The theorem `Finset.image_singleton` states that for any types `α` and `β`, where `β` has decidable equality, and for any function `f` from `α` to `β` and any element `a` of type `α`, the image of the singleton set `{a}` under the function `f` is the singleton set containing `f(a)`. In other words, applying the function `f` to each element of the singleton set `{a}` yields a new singleton set `{f(a)}`.
More concisely: For any types `α` and `β` with decidable equality, and for any function `f` from `α` to `β` and element `a` of type `α`, the image of the singleton set `{a}` under `f` is the singleton set `{f(a)}`.
|
Mathlib.Data.Finset.Image._auxLemma.25
theorem Mathlib.Data.Finset.Image._auxLemma.25 :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {b : β},
(b ∈ Finset.image f s) = ∃ a ∈ s, f a = b
This theorem, `Mathlib.Data.Finset.Image._auxLemma.25`, states that for any types `α` and `β`, where `β` has decidable equality, a function `f` from `α` to `β`, a finite set `s` of type `α`, and an element `b` of type `β`, `b` is in the image of `s` under `f` if and only if there exists an element `a` in `s` such that `f(a)` equals `b`. In other words, an element is in the image of a set under a function if and only if it is the output of the function applied to an element of the original set.
More concisely: For any type `α`, `β` with decidable equality, and a function `f` from `α` to `β`, an element `b` is in the image of a finite set `s` of type `α` under `f` if and only if there exists an element `a` in `s` such that `f(a) = b`.
|
Finset.mem_map'
theorem Finset.mem_map' :
∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) {a : α} {s : Finset α}, f a ∈ Finset.map f s ↔ a ∈ s
The theorem `Finset.mem_map'` states that for all types `α` and `β`, and for all embedding function `f` from `α` to `β`, an element `a` of type `α`, and a finset `s` of type `α`, the element `f a` is in the image of the finset `s` under the function `f` if and only if the element `a` is in the finset `s`. In other words, this theorem provides a condition to check if an element is in the image of a finset under an embedding function.
More concisely: For all types `α` and `β`, and for all embedding functions `f` from `α` to `β`, if `a` is an element of finset `s` of type `α`, then `f a` is an element of the image of `s` under `f`. Conversely, if `f a` is an element of the image of `s`, then `a` is an element of `s`.
|
Finset.subtype_map
theorem Finset.subtype_map :
∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] {s : Finset α},
Finset.map (Function.Embedding.subtype p) (Finset.subtype p s) = Finset.filter p s
The theorem `Finset.subtype_map` states that for any type `α`, a predicate `p` on `α` (where `p` is a decidable predicate), and a `Finset` `s` of `α`, if we first convert `s` into a finset of subtypes that satisfy predicate `p` using `s.subtype p`, and then map it back to type `α` using the subtype embedding `Function.Embedding.subtype p`, we get the same finset as if we had directly filtered `s` with predicate `p` using `Finset.filter p s`. In other words, filtering a finset `s` by a predicate `p` is equivalent to first taking the subtype according to `p`, and then embedding it back to the original type.
More concisely: For any type `α`, decidable predicate `p` on `α`, and `Finset` `s` of `α`, the map of the subtype `s.subtype p` to `α` through the subtype embedding is equal to the filtering of `s` with the predicate `p`.
|
Multiset.toFinset_map
theorem Multiset.toFinset_map :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] (f : α → β) (m : Multiset α),
(Multiset.map f m).toFinset = Finset.image f m.toFinset
The theorem `Multiset.toFinset_map` states that for all types `α` and `β` and for all functions `f` mapping `α` to `β`, as well as for all multisets `m` of type `α`, applying the function `f` to each element of the multiset `m` and then removing duplicates (using `Multiset.map` followed by `Multiset.toFinset`) is equivalent to first removing duplicates from the multiset `m` and then applying the function `f` to each element of the resulting finset (using `Multiset.toFinset` followed by `Finset.image`). This is under the condition that equality is decidable for both `α` and `β`. In other words, the order of removing duplicates (via `toFinset`) and applying the function `f` (via `map` or `image`) doesn't matter.
More concisely: For all types `α` and `β` with decidable equality, the functions `Multiset.toFinset.image` and `Multiset.map` followed by `Finset.image` are equal for multisets `m` of type `α` and functions `f` from `α` to `β`.
|
Finset.property_of_mem_map_subtype
theorem Finset.property_of_mem_map_subtype :
∀ {α : Type u_1} {p : α → Prop} (s : Finset { x // p x }) {a : α},
a ∈ Finset.map (Function.Embedding.subtype fun x => p x) s → p a
The theorem `Finset.property_of_mem_map_subtype` states that for any type `α`, a property `p` of `α`, a finset `s` of the subtype of `α` satisfying `p`, and any element `a` of type `α`, if `a` is in the finset obtained by mapping `s` to `α` using the subtype embedding function (`Function.Embedding.subtype`), then `a` must satisfy property `p`. In other words, all elements of the finset obtained by converting a finset of a subtype to the main type using the subtype embedding, retain the property of the subtype.
More concisely: Given a subtype `s` of type `α` with property `p`, and the image `t` of `s` under the subtype embedding function, if an element `a` is in `t`, then `a` has property `p`.
|
Finset.subset_image_iff
theorem Finset.subset_image_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {s : Set α} {t : Finset β} {f : α → β},
↑t ⊆ f '' s ↔ ∃ s', ↑s' ⊆ s ∧ Finset.image f s' = t
This theorem states that, given a type `α`, a type `β`, a set `s` of type `α`, a finite set `t` of type `β`, and a function `f` from `α` to `β`, the statement that `t` is a subset of the image of `s` under `f` is equivalent to the existence of a finite subset `s'` of `s` such that the image of `s'` under `f` equals `t`. In other words, any subset of the image of a set under a function is exactly the image of a subset of the original set under the same function. This theorem is valid under the assumption that the equality of elements of `β` is decidable.
More concisely: Given sets `α`, `β`, a type `s ⊆ α`, a finite set `t ⊆ β`, and a function `f : α → β`, the sets `t ⊆ Img (f `` s)` if and only if there exists a finite `s' ⊆ s` such that `t = Img (f `` s')`.
|
Finset.image_subset_image_iff
theorem Finset.image_subset_image_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s t : Finset α},
Function.Injective f → (Finset.image f s ⊆ Finset.image f t ↔ s ⊆ t)
The theorem `Finset.image_subset_image_iff` states that for any two finite sets `s` and `t` of an arbitrary type `α`, and a function `f` from `α` to another arbitrary type `β`, given that `f` is injective and that equality on `β` is decidable, the preimage of `s` under `f` is a subset of the preimage of `t` under `f` if and only if `s` is a subset of `t`. In simpler terms, if `f` is a function that doesn't map different elements to the same element (injective) and we can decide whether two elements of `β` are equal, then the image of a smaller set `s` under `f` is always a subset of the image of a larger set `t` under `f`.
More concisely: For injective functions between arbitrary types with decidable equality on the codomain, the preimage of a smaller set under the function is a subset of the preimage of a larger set if and only if the smaller set is a subset of the larger set.
|
Finset.image_inter
theorem Finset.image_inter :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} [inst_1 : DecidableEq α] (s₁ s₂ : Finset α),
Function.Injective f → Finset.image f (s₁ ∩ s₂) = Finset.image f s₁ ∩ Finset.image f s₂
The theorem `Finset.image_inter` states that for any two sets `s₁` and `s₂` of an arbitrary type `α`, and a function `f` from `α` to another type `β`, provided that `f` is injective and the equality in `β` is decidable, the image of the intersection of `s₁` and `s₂` under `f` is the same as the intersection of the images of `s₁` and `s₂` under `f`. In other words, if `f` is an injective function, it preserves the intersection operation when it is applied to sets. This theorem is a formal statement of the property in set theory that the image of the intersection is the intersection of the images for an injective function.
More concisely: If `f` is an injective function between sets `α` with decidable equality, then `f` preserves the intersection operation, i.e., `f(s₁ ∩ s₂) = f(s₁) ∩ f(s₂)` for any sets `s₁, s₂ ⊆ α`.
|
Finset.mem_image
theorem Finset.mem_image :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {b : β},
b ∈ Finset.image f s ↔ ∃ a ∈ s, f a = b
The theorem `Finset.mem_image` states that for any types `α` and `β`, given a decidable equality on `β`, a function `f` from `α` to `β`, a finite set `s` of type `α`, and an element `b` of type `β`, `b` is in the image of `s` under `f` if and only if there exists an element `a` in `s` such that `f(a) = b`. In other words, an element `b` is in the image of `s` under `f` exactly when `b` is the image of some element in `s` under the function `f`.
More concisely: For any decidable equality on type `β` and a function `f` from type `α` to `β`, an element `b` is in the image of a finite set `s` of type `α` under `f` if and only if there exists an element `a` in `s` such that `f(a) = b`.
|
Finset.image_sdiff
theorem Finset.image_sdiff :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : DecidableEq α] {f : α → β} (s t : Finset α),
Function.Injective f → Finset.image f (s \ t) = Finset.image f s \ Finset.image f t
This theorem states that for any two finite sets `s` and `t` of type `α`, and a function `f` from `α` to `β` that is injective (i.e., it assigns a unique value in `β` to each element in `α`), the image of the difference of `s` and `t` under `f` (i.e., `f` applied to each element of `s \ t`) is equal to the difference of the images of `s` and `t` under `f`. In other words, `f` preserves the operation of set difference. This requires that equality is decidable for both `α` and `β`, which means given any two elements of the same type, we can decide whether they are equal or not. The theorem can be succinctly expressed in mathematical terms as: if `f` is injective, then `f(s \ t) = f(s) \ f(t)`.
More concisely: If `f` is an injective function from a finite set `α` to `β` with decidable equality, then `f(s \ t) = f(s) \ f(t)` for any finite sets `s` and `t` in `α`.
|
Finset.image_filter
theorem Finset.image_filter :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {p : β → Prop}
[inst_1 : DecidablePred p],
Finset.filter p (Finset.image f s) = Finset.image f (Finset.filter (fun a => p (f a)) s)
The theorem `Finset.image_filter` states that for any two types `α` and `β`, where `β` has decidable equality, and for any function `f` from `α` to `β`, any finite set `s` of elements of type `α`, and any predicate `p` on `β` that is a decidable predicate, the result of filtering `p` on the image of `s` under `f` is equal to the image under `f` of the result of filtering `s` on the predicate that applies `p` to `f(a)` for each `a` in `α`. In simpler terms, it asserts that the order of filtering and mapping does not matter.
More concisely: For any decidable predicate `p` on type `β`, function `f` from `α` to `β`, finite set `s` of elements in `α`, the image of filtering `s` on `p` under `f` is equal to the filtering of `f(s)` on `p`.
|
Mathlib.Data.Finset.Image._auxLemma.32
theorem Mathlib.Data.Finset.Image._auxLemma.32 :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α}, f '' ↑s = ↑(Finset.image f s)
This theorem establishes that for any two types `α` and `β` where `β` has a decidable equality, and for any function `f` mapping `α` to `β` and any finite set `s` of type `α`, the image of `s` under the function `f` (denoted as `f '' ↑s`) is equal to the forward image of `s` under `f` converted to a set (denoted as `↑(Finset.image f s)`). In other words, applying `f` to each element of the set `s` produces the same result whether you treat `s` as a finite set or as a general set.
More concisely: For any function `f` from type `α` to decidably equal types `β`, and any finite set `s` of type `α`, `f '' ↑s` equals `↑(Finset.image f s)`.
|
Finset.map_disjUnion'
theorem Finset.map_disjUnion' :
∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} (s₁ s₂ : Finset α) (h' : Disjoint (Finset.map f s₁) (Finset.map f s₂))
(h : optParam (Disjoint s₁ s₂) ⋯),
Finset.map f (s₁.disjUnion s₂ h) = (Finset.map f s₁).disjUnion (Finset.map f s₂) h'
The theorem `Finset.map_disjUnion'` states that if we have two finsets `s₁` and `s₂` of a type `α`, along with an embedding `f` from `α` to `β`, and if the images of `s₁` and `s₂` under `f` are disjoint (in the sense that their infimum in the lattice structure is the bottom element), then the image under `f` of the disjoint union of `s₁` and `s₂` (where the disjointness of `s₁` and `s₂` could be provided optionally) is equal to the disjoint union of the images of `s₁` and `s₂` under `f`. This gives a condition under which the mapping function `f` commutes with the operation of taking the disjoint union of finsets.
More concisely: If `s₁` and `s₂` are disjoint finsets of type `α` and their images under an embedding `f` from `α` to `β` are disjoint, then `f` maps the disjoint union of `s₁` and `s₂` to the disjoint union of `f(s₁)` and `f(s₂)`.
|
Finset.image_val
theorem Finset.image_val :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α → β) (s : Finset α),
(Finset.image f s).val = (Multiset.map f s.val).dedup
The theorem `Finset.image_val` states that for all types `α` and `β`, given a decidable equality on `β`, a function `f` mapping from `α` to `β`, and a finite set `s` of type `α`, the value of the image of `s` under `f` (computed using `Finset.image`) is equal to the multiset resulting from removing duplicates (using `Multiset.dedup`) from the multiset obtained by mapping `f` over the value of `s` (using `Multiset.map`). Essentially, it's defining what it means to apply a function to each element of a finite set: we get a new finite set with no duplicates, where each element is the result of applying the function to an element of the original set.
More concisely: For any types `α` and `β`, given a decidable equality on `β` and a function `f` from `α` to `β`, the image of a finite set `s` under `f`, computed as `Finset.image s f`, is equal to the multiset obtained by mapping `f` over `s` and removing duplicates, denoted as `Multiset.dedup (Multiset.map f s)`.
|
Finset.mem_map
theorem Finset.mem_map :
∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {b : β}, b ∈ Finset.map f s ↔ ∃ a ∈ s, f a = b := by
sorry
The theorem `Finset.mem_map` states that for any types `α` and `β`, any embedding `f` from `α` to `β`, any finite set `s` of type `α`, and any element `b` of type `β`, `b` is in the image of the finite set `s` under the embedding `f` if and only if there exists an element `a` in `s` such that `f(a) = b`. In other words, an element is in the image of a finite set under an embedding if and only if it is the image of some element in the original set under the embedding.
More concisely: For any finite set $S \subseteq \alpha$, embedding $f : \alpha \to \beta$, and $\beta$-element $b$, $b \in \operatorname{image}(f(S))$ if and only if $\exists a \in S. \, f(a) = b$.
|
Finset.map_nonempty
theorem Finset.map_nonempty :
∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α}, (Finset.map f s).Nonempty ↔ s.Nonempty
The theorem `Finset.map_nonempty` states that for any types `α` and `β`, for any embedding `f` from `α` to `β`, and for any finset `s` of type `α`, the mapped finset `Finset.map f s` is nonempty if and only if the original finset `s` is nonempty. In other words, the image of a nonempty finset under an embedding is nonempty, and a finset has a nonempty image under an embedding only if it is nonempty itself.
More concisely: Given an embedding `f` from type `α` to `β` and a nonempty finset `s` of type `α`, the image `Finset.map f s` is also a nonempty finset.
|
Finset.biUnion_singleton
theorem Finset.biUnion_singleton :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {s : Finset α} {f : α → β},
(s.biUnion fun a => {f a}) = Finset.image f s
The theorem `Finset.biUnion_singleton` states that for any finite set `s` of a type `α`, with a function `f` from `α` to another type `β` where `β` has decidable equality, the union of singletons `{f a}` for every `a` in `s` (expressed as `Finset.biUnion s fun a => {f a}` in Lean) is equal to the image of `s` under the function `f` (expressed as `Finset.image f s` in Lean). This theorem essentially verifies a key property of images of sets in the context of finite sets in Lean.
More concisely: For any finite set `s` and function `f` from a type `α` to a type `β` with decidable equality, the union of the singletons `{f a}` for each `a` in `s` equals the image `Finset.image f s` of `s` under `f`.
|
Finset.map_eq_image
theorem Finset.map_eq_image :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α ↪ β) (s : Finset α),
Finset.map f s = Finset.image (⇑f) s
The theorem `Finset.map_eq_image` states that for any two types `α` and `β` with `β` having decidable equality, and for any embedding function `f` from `α` to `β` and a finite set `s` of type `α`, the image of `s` under `f` obtained through the `map` function is the same as the image obtained through the `image` function. In other words, both operations `map` and `image` provide the same result when transforming a finite set via an embedding function. This is useful because it provides flexibility to use either the `map` or `image` function based on specific requirements without affecting the outcome.
More concisely: For any finite set `s` of type `α` and an embedding function `f` from `α` to `β` with decidable equality, `map f s` equals `image f s`.
|
Mathlib.Data.Finset.Image._auxLemma.21
theorem Mathlib.Data.Finset.Image._auxLemma.21 : ∀ {n m : ℕ}, (m ∈ Finset.range n) = (m < n)
This theorem, `Mathlib.Data.Finset.Image._auxLemma.21`, states that for any two natural numbers `n` and `m`, the membership of `m` in the set `Finset.range n` is equivalent to the condition that `m` is less than `n`. In other words, `m` belongs to the set of natural numbers less than `n` if and only if `m` is strictly less than `n`.
More concisely: For any natural numbers `n` and `m`, `m` belongs to the finite set of natural numbers `{i : Nat | i < n}` if and only if `m` is strictly less than `n`.
|
Finset.mem_image_of_mem
theorem Finset.mem_image_of_mem :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {s : Finset α} (f : α → β) {a : α},
a ∈ s → f a ∈ Finset.image f s
The theorem `Finset.mem_image_of_mem` states that for every types `α` and `β` with `β` being a type with decidable equality, every finite set `s` of type `α`, and every function `f` from `α` to `β`, if an element `a` of type `α` belongs to the set `s`, then the image of `a` under `f` belongs to the image of the set `s` under `f`. In other words, if `a` is in a finite set `s`, then its image `f(a)` is in the image of the set `s` under the function `f`.
More concisely: If `α` is a type with decidable equality, `s : Finset α`, `f : α → β`, and `a ∈ s`, then `f(a) ∈ image f s`.
|
Finset.not_mem_map_subtype_of_not_property
theorem Finset.not_mem_map_subtype_of_not_property :
∀ {α : Type u_1} {p : α → Prop} (s : Finset { x // p x }) {a : α},
¬p a → a ∉ Finset.map (Function.Embedding.subtype fun x => p x) s
The theorem `Finset.not_mem_map_subtype_of_not_property` states that for any type `α` and a property `p` on `α`, for any subset `s` of `α` consisting only of elements that satisfy the property `p`, and for any element `a` of `α` that does not satisfy `p`, if we convert the subset `s` to a `Finset` of the main type `α` using the `Embedding.subtype` function, then the resulting `Finset` will not contain the element `a`. In other words, the image of a `Finset` under the function `Function.Embedding.subtype` does not contain any elements that do not satisfy the property of the subtype.
More concisely: For any subset `s` of type `α` consisting only of elements satisfying property `p`, and any `a` not satisfying `p` in `α`, `Embedding.subtype s` does not contain `a`.
|
Finset.subset_map_symm
theorem Finset.subset_map_symm :
∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {f : α ≃ β},
s ⊆ Finset.map f.symm.toEmbedding t ↔ Finset.map f.toEmbedding s ⊆ t
This theorem is a version of `Equiv.subset_symm_image` specifically for `Finset` and states that for any types `α` and `β`, any `Finset` `s` in `α`, any `Finset` `t` in `β`, and any bijective function `f` from `α` to `β`, `s` is a subset of the image of `t` under the inverse of `f` if and only if the image of `s` under `f` is a subset of `t`. Essentially, it describes a relationship between the images of sets under the function and its inverse.
More concisely: For any types α and β, any bijective function f between Finsets s in α and t in β, the inverse image of t under f equals the image of s under f. In other words, s ↦ f⁻¹(t) if and only if f(s) ⊆ t.
|
Finset.subtype_map_of_mem
theorem Finset.subtype_map_of_mem :
∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Finset α},
(∀ x ∈ s, p x) → Finset.map (Function.Embedding.subtype p) (Finset.subtype p s) = s
The theorem `Finset.subtype_map_of_mem` states that for any given type `α` and a predicate `p` that can be decided for elements of `α`, if every element `x` of a given finset `s` satisfies the predicate `p`, then mapping the finset `s` to the subtype of `p` using `Finset.subtype` and then converting it back to the original finset using `Function.Embedding.subtype` will give us back the original finset `s`. This basically means that the process of converting a finset to a subtype and then back to the original finset is a lossless operation when all elements of the finset satisfy the given predicate.
More concisely: If `s` is a finset of type `α` and `p` is a decidable predicate on `α` such that `p(x)` holds for all `x` in `s`, then `Function.Embedding.subtype (Finset.subtype p s) = s`.
|
Finset.map_subset_map
theorem Finset.map_subset_map :
∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s₁ s₂ : Finset α}, Finset.map f s₁ ⊆ Finset.map f s₂ ↔ s₁ ⊆ s₂ := by
sorry
This theorem states that for any types `α` and `β`, and an embedding `f` from `α` to `β`, if `s₁` and `s₂` are two finsets in `α`, then the image of `s₁` under the map `f` is a subset of the image of `s₂` under the map `f` if and only if `s₁` is a subset of `s₂`. In simpler terms, this theorem ensures that the subset relation between two finsets is preserved when they are mapped to another type under an embedding.
More concisely: For any types `α`, `β`, andembedding `f` from `α` to `β`, if `s₁` and `s₂` are finsets in `α`, then `f(s₁) ⊆ f(s₂)` if and only if `s₁ ⊆ s₂`.
|
Finset.coe_image
theorem Finset.coe_image :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α}, ↑(Finset.image f s) = f '' ↑s
The theorem `Finset.coe_image` states that for any types `α` and `β`, where `β` has a decidable equality, and for any function `f` from `α` to `β` and any finite set `s` of type `α`, the co-domain of the image of the function `f` applied to the set `s` is equal to the image of the function `f` applied to the co-domain of `s`. In mathematical terms, this is equivalent to saying that for a function $f: α \to β$ and a finite set $s \subseteq α$, the set of all $f(x)$ for $x \in s$ is the same whether we consider $s$ as a finset or as a set.
More concisely: For any function $f: α \to β$ with decidable equality and finite set $s \subseteq α$, the image of $f$ applied to the co-domain of $s$ is equal to the co-domain of the image of $f$ applied to $s$.
|
Finset.map_val
theorem Finset.map_val :
∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α), (Finset.map f s).val = Multiset.map (⇑f) s.val := by
sorry
The theorem `Finset.map_val` states that for any types `α` and `β` and any embedding function `f` from `α` to `β`, when this function is applied to a finset `s` of type `α` using `Finset.map`, the underlying multiset of the resulting finset is equal to the multiset obtained by applying `Multiset.map` with `f` to the underlying multiset of `s`. In other words, the operation of mapping a function over a finset behaves the same as mapping the same function over the underlying multiset of that finset.
More concisely: For any types `α` and `β`, and any embedding function `f` from `α` to `β`, the map operation on a finset `s` of type `α` using `Finset.map` is equivalent to applying `Multiset.map` with `f` to the underlying multiset of `s`.
|
Finset.image_eq_empty
theorem Finset.image_eq_empty :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α}, Finset.image f s = ∅ ↔ s = ∅
This theorem states that for any types `α` and `β`, and any function `f` from `α` to `β`, the image of a finite set `s` under the function `f` is empty if and only if the original set `s` is empty. In mathematical terms, for a function `f: α → β` and a set `s ⊆ α`, `f(s) = ∅` if and only if `s = ∅`. This relies on the fact that equality is decidable in `β`.
More concisely: For any function `f: α → β` and set `s ⊆ α`, `f(s) = ∅` if and only if `s = ∅`, given decidable equality in `β`.
|
Finset.fiber_nonempty_iff_mem_image
theorem Finset.fiber_nonempty_iff_mem_image :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α → β) (s : Finset α) (y : β),
(Finset.filter (fun x => f x = y) s).Nonempty ↔ y ∈ Finset.image f s
The theorem `Finset.fiber_nonempty_iff_mem_image` states that for any types `α` and `β` with decidable equality on `β`, any function `f` from `α` to `β`, any finite set `s` of `α`, and any element `y` of `β`, the fiber of `f` over `y` in `s` (i.e., the set of elements of `s` mapped to `y` by `f`) is nonempty if and only if `y` is in the image of `f` on `s`. In other words, there is an element of `s` that `f` maps to `y` if and only if `y` is a value `f` takes on `s`.
More concisely: For any function `f` from type `α` to type `β` with decidable equality on `β`, a finite set `s` of `α`, and an element `y` of `β`, the fiber of `f` over `y` in `s` is nonempty if and only if `y` is in the image of `f` on `s`.
|
Finset.image_subset_iff
theorem Finset.image_subset_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β},
Finset.image f s ⊆ t ↔ ∀ x ∈ s, f x ∈ t
The `Finset.image_subset_iff` theorem states that for any types `α` and `β`, and given a function `f : α → β`, a finite set `s` of type `α` and a finite set `t` of type `β`, the image of `s` under the function `f` is a subset of `t` if and only if for every element `x` in `s`, the image of `x` under `f` is in `t`. Here, the image of a set under a function, denoted as `Finset.image f s`, is a set consisting of all the images of the elements of the original set under the function, and `DecidableEq β` indicates that equality between elements of `β` can be decided. The subset relation, denoted as `⊆`, is a binary relation between two sets that expresses the fact that every element of the first set is also an element of the second set.
More concisely: For any functions `f : α → β` between types, finite sets `s : Finset α`, and `t : Finset β`, `Finset.image s f ⊆ t` if and only if for all `x ∈ s`, `f x ∈ t`.
|
Finset.mem_map_of_mem
theorem Finset.mem_map_of_mem :
∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) {a : α} {s : Finset α}, a ∈ s → f a ∈ Finset.map f s
This theorem states that for any types `α` and `β`, if `f` is an embedding from `α` to `β`, `a` is an element of the finset `s` in `α`, then the image of `a` under the embedding `f` is an element of the image finset `Finset.map f s` in `β`. In other words, if an element is in a finset, then its image under a given embedding function is in the mapped finset. This is a fundamental property about the interaction of embeddings and finsets in Lean 4.
More concisely: For any embeddings between types `f : α → β` and finsets `s : Finset α`, if `a ∈ s`, then `f a ∈ Finset.map f s`.
|
Finset.mem_range_iff_mem_finset_range_of_mod_eq'
theorem Finset.mem_range_iff_mem_finset_range_of_mod_eq' :
∀ {α : Type u_1} [inst : DecidableEq α] {f : ℕ → α} {a : α} {n : ℕ},
0 < n → (∀ (i : ℕ), f (i % n) = f i) → (a ∈ Set.range f ↔ a ∈ Finset.image (fun i => f i) (Finset.range n))
This theorem states that for any type `α` with decidable equality, a function `f` from natural numbers to `α`, an element `a` of `α`, and a natural number `n` larger than 0, if `f` satisfies the property that the value of `f` at `i` is equal to the value of `f` at `i mod n` for every natural number `i`, then `a` is in the range of `f` if and only if `a` is in the image of `f` when applied to the set of natural numbers less than `n`. In other words, when the function `f` has a periodic behavior with period `n`, we can restrict the domain to the first `n` natural numbers without losing any values in the range.
More concisely: If `f:` ℕ -> α is a function with decidable equality, `a:` α, and `n:` ℕ > 0 such that `f` is periodic with period `n`, then `a` is in the range of `f` if and only if `a` is in the image of `f` restricted to the natural numbers less than `n`.
|
Finset.image_empty
theorem Finset.image_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α → β), Finset.image f ∅ = ∅
This theorem states that for any types `α` and `β`, and any function `f` from `α` to `β` where `β` has decidable equality, the image of the empty set under this function `f` is also the empty set. In other words, if you apply a function to each element of an empty set, the resulting set is still empty, regardless of the function. This is because there are no elements in the empty set to which the function can be applied.
More concisely: For any types `α` and `β` and decidably equal function `f : α → β`, the image of the empty set under `f` is empty.
|
Finset.filter_map
theorem Finset.filter_map :
∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {p : β → Prop} [inst : DecidablePred p],
Finset.filter p (Finset.map f s) = Finset.map f (Finset.filter (p ∘ ⇑f) s)
The theorem `Finset.filter_map` states that for any given types `α` and `β`, embedding function `f` from `α` to `β`, finset `s` of type `α`, and a decidable property `p` for type `β`, the filter of `p` applied to the map of `f` over `s` is equivalent to the map of `f` over the filter of `p` composed with `f` applied to `s`. In simpler terms, it means you can either first map a function over a finset and then filter the results, or first filter the finset and then map the function, and both processes will yield the same result.
More concisely: For any type `α`, type `β`, decidable property `p` on `β`, embedding function `f` from `α` to `β`, and finset `s` of type `α`, the filter of `p` applied to the image of `s` under `f` is equal to the image of the filter of `p` composed with `f` applied to `s`.
|