Finset.sup_eq_iSup
theorem Finset.sup_eq_iSup :
∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] (s : Finset α) (f : α → β), s.sup f = ⨆ a ∈ s, f a := by
sorry
The theorem `Finset.sup_eq_iSup` states that for all types α and β, where β is a complete lattice, given a finite set `s` of type α and a function `f` from α to β, the supremum of the finite set `s` under function `f` is equal to the supremum over all elements `a` that belong to the set `s` of `f(a)`. In mathematical terms, it means `sup {a, b, c} f = ⨆ a ∈ {a, b, c}, f a` where `⨆` represents the supremum.
More concisely: For any complete lattice β and a finite set s of type α with function f from α to β, the supremum of set s under function f equals the supremum of the images of individual set elements under f. That is, sup(s.map(f)) = ⨆ x ∈ s, f x.
|
Finset.sup'_map
theorem Finset.sup'_map :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] {s : Finset γ} {f : γ ↪ β} (g : β → α)
(hs : (Finset.map f s).Nonempty), (Finset.map f s).sup' hs g = s.sup' ⋯ (g ∘ ⇑f)
The theorem `Finset.sup'_map` states that for any types `α`, `β`, and `γ`, given `α` forms a semilattice under the operation `sup`, a finite subset `s` of `γ`, an embedding `f` from `γ` to `β`, and a function `g` from `β` to `α`, if the image of `s` under `f` is nonempty, then the supremum of the image of `s` under `f`, computed using `g`, is the same as the supremum of `s` computed using `g` composed with `f`. Essentially, this theorem is saying that mapping a finite set and then taking the supremum is the same as first taking the supremum and then applying the map, given that the set is nonempty.
More concisely: Given a semilattice `α` with operation `sup`, an embedding `f` from `γ` to `β`, a finite subset `s` of `γ`, and a function `g` from `β` to `α`, if `s` has a nonempty image under `f`, then `sup (g ∘ f"" s) = sup (g"" s)`.
|
Finset.min'_singleton
theorem Finset.min'_singleton : ∀ {α : Type u_2} [inst : LinearOrder α] (a : α), {a}.min' ⋯ = a
This theorem states that for any given type `α` equipped with a linear order, the minimum element of a singleton set, i.e., a set containing only one element `a` of type `α`, is `a` itself. In other words, if you have a set with only one element and you ask for the minimum element of that set, you always get the element itself, irrespective of what the element is or what type it belongs to, as long as the type has a linear order defined on it.
More concisely: For any type `α` with a linear order, the minimum element of a singleton set is its unique element.
|
Finset.sup_coe
theorem Finset.sup_coe :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {P : α → Prop} {Pbot : P ⊥}
{Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)} (t : Finset β) (f : β → { x // P x }),
↑(t.sup f) = t.sup fun x => ↑(f x)
This theorem states that for any finset `t` of type `β` and a function `f` mapping from `β` to a subtype of `α` satisfying a property `P`, the supremum (or greatest element) of `t` computed within this subtype is the same as computing the supremum in `α` itself. The property `P` must hold for `⊥` (the bottom element in a bounded lattice) and be closed under the sup operation, i.e., if `P` holds for `x` and `y`, it must also hold for their supremum `x ⊔ y`.
More concisely: For any finset `t` of type `β` and a monotone function `f` from `β` to a lattice `α` such that `f(⊥)` exists and `P(f(x))` holds for all `x` in `β` with `P` being a closed sublattice property, `f(����(t))` equals `����(f(``t``))`, where `����` denotes the supremum or greatest element in their respective lattices.
|
Mathlib.Data.Finset.Lattice._auxLemma.4
theorem Mathlib.Data.Finset.Lattice._auxLemma.4 :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {a : α},
(s.sup f ≤ a) = ∀ b ∈ s, f b ≤ a
This theorem states that for all types `α` and `β`, given a semilattice-supremum structure and an order-bottom structure on `α`, a finite set `s` of type `β`, a function `f` from `β` to `α`, and an element `a` of type `α`, the supremum of the images of the elements of `s` under `f` is less than or equal to `a` if and only if for every element `b` in `s`, the image of `b` under `f` is less than or equal to `a`. In other words, `a` is an upper bound for the image of the set `s` under `f` in the order structure of `α` if and only if `a` is an upper bound for each element in the image of `s` under `f`.
More concisely: For all types `α` and `β`, given a semilattice-supremum and order-bottom structure on `α`, a finite set `s` of type `β`, a function `f` from `β` to `α`, and an element `a` of type `α`, the image of the supremum of `s` under `f` is less than or equal to `a` if and only if every image of an element in `s` under `f` is less than or equal to `a`.
|
Finset.induction_on_max
theorem Finset.induction_on_max :
∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : DecidableEq α] {p : Finset α → Prop} (s : Finset α),
p ∅ → (∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → p s → p (insert a s)) → p s
The theorem `Finset.induction_on_max` provides an induction principle for finite sets (`Finset`s) over a linearly ordered type. It states that for a given property `p` and a finite set `s` of a linearly ordered type `α` with decidable equality, if the property holds for the empty set, and for any element `a` strictly greater than all elements in the set `s`, the property `p` holding for `s` implies that the property `p` also holds for the set that results from inserting `a` into `s`, then the property `p` holds for the initial set `s`. This theorem essentially allows us to prove properties about all finite sets in a linearly ordered type by starting with the empty set and then considering sets with progressively larger maximum elements.
More concisely: Given a property `p` and a finite set `s` in a linearly ordered type `α` with decidable equality, if `p` holds for the empty set and for all `a` greater than all elements in `s`, `p` holds for `s` implies `p` holds for `s.insert a`, then `p` holds for `s`.
|
Finset.isLeast_min'
theorem Finset.isLeast_min' :
∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty), IsLeast (↑s) (s.min' H)
This theorem states that for any non-empty finset `s` in a linearly ordered type `α`, the minimum element of `s` is a least element of the set. Here, being a "least element" means that the element not only belongs to the set, but is also lower than or equal to all other elements in the set (i.e., it falls within the lower bounds of the set). The function `Finset.min'` is used to obtain the minimum element of the finset, and `IsLeast` is used to assert its status as the least element.
More concisely: For any non-empty finset `s` in a linearly ordered type `α`, the minimum element of `s` is the unique element that is both in `s` and less than or equal to every other element in `s`.
|
Finset.max'_mem
theorem Finset.max'_mem : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty), s.max' H ∈ s := by
sorry
The theorem `Finset.max'_mem` states that for any non-empty finite set `s` in a linearly ordered type `α`, the maximum element of `s`, denoted by `Finset.max' s H`, belongs to `s` itself. Here, `H` is a proof confirming that the set `s` is non-empty.
More concisely: For any non-empty finite set `s` in a linearly ordered type `α`, the maximum element of `s` is an element of `s`.
|
Monotone.map_finset_max'
theorem Monotone.map_finset_max' :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
Monotone f → ∀ {s : Finset α} (h : s.Nonempty), f (s.max' h) = (Finset.image f s).max' ⋯
This theorem states that for any function `f` from a type `α` to a type `β`, both equipped with a linear order, if `f` is monotone, then for any nonempty set `s` of type `α`, the maximum element of `s` under the function `f` is the same as the maximum element of the image of `s` under `f`. In other words, applying a monotone function to the maximum element of a nonempty set results in the maximum element of the set's image under the function.
More concisely: If `f: α → β` is a monotone function between ordered types `α` and `β`, then for any nonempty `s ⊆ α`, the maximum element of `s` is the maximum of `f''s`.
|
Mathlib.Data.Finset.Lattice._auxLemma.17
theorem Mathlib.Data.Finset.Lattice._auxLemma.17 :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (f : β → α) (S : Finset β),
(S.sup f = ⊥) = ∀ s ∈ S, f s = ⊥
This theorem states that for any types `α` and `β` with `α` being a semilattice sup and order bot, and given a function `f` from `β` to `α` and a finite set `S` of type `β`, the supremum of the set `S` under the function `f` is equal to the bottom element of `α` if and only if for every element `s` in `S`, the value of the function `f` at `s` is equal to the bottom element of `α`. In other words, all elements of `S` map to the least element in `α` under function `f` if the supremum of the mapped set is also the least element in `α`.
More concisely: For any semilattice sup and order bot types `α` and `β`, function `f`: `β → α`, and finite set `S` ⊆ `β`, if for all `s` ∈ `S`, `f(s)` = bot(`α`), then `sup(map(f, S))` = bot(`α`).
|
Finset.le_sup
theorem Finset.le_sup :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {b : β},
b ∈ s → f b ≤ s.sup f
The theorem `Finset.le_sup` states that for any types `α` and `β`, given a semilattice structure and a bottom element on `α`, a finite set `s` of `β`, a function `f` from `β` to `α`, and an element `b` of `β`, if `b` belongs to the set `s`, then the value of the function `f` at `b` is less than or equal to the supremum of the values of `f` over the set `s`. In other words, for all elements in a set, the function value at each element is always less than or equal to the supremum (greatest value) of the function values at all elements in the set.
More concisely: For any semilattice `α` with bottom element, function `f` from a finite set `s` of type `β` to `α`, and element `b` in `s`, we have `f b ≤ sup (map f s)`.
|
Mathlib.Data.Finset.Lattice._auxLemma.2
theorem Mathlib.Data.Finset.Lattice._auxLemma.2 : ∀ {a b c : Prop}, (a ∧ b → c) = (a → b → c)
This theorem, `Mathlib.Data.Finset.Lattice._auxLemma.2`, states that for any three propositions `a`, `b`, and `c`, the implication `(a ∧ b → c)` is equivalent to `(a → b → c)`. That is to say, if we assume that `a` and `b` together imply `c`, this is the same as saying that if `a` is true, then `b` implies `c`. This captures the intuition that the truth of `c` follows from the combined truth of `a` and `b`, regardless of how those assumptions are structured.
More concisely: The theorem `Mathlib.Data.Finset.Lattice._auxLemma.2` asserts that the logical implications `(a ∧ b → c)` and `(a → (b → c))` are equivalent for any propositions `a`, `b`, and `c`.
|
Finset.iSup_insert
theorem Finset.iSup_insert :
∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] [inst_1 : DecidableEq α] (a : α) (s : Finset α)
(t : α → β), ⨆ x ∈ insert a s, t x = t a ⊔ ⨆ x ∈ s, t x
The theorem `Finset.iSup_insert` states that for any types `α` and `β`, where `β` forms a complete lattice, and for any decidable equality on `α`, if we have a function `t` from `α` to `β`, an element `a` of type `α`, and a finite set `s` of type `α`, then the supremum (i.e., the least upper bound) of the function `t` over the set obtained by inserting `a` into `s` is equal to the supremum of `t a` and the supremum of `t` over `s`. In other words, adding an element to a finite set and taking the supremum does not change the value if the supremum was already taken of the set and the element.
More concisely: For any complete lattice β and decidable equality on type α, if t is a function from α to β, a is an element of α, and s is a finite set of α, then the supremum of t over s with a inserted is equal to the supremum of t(a) and the supremum of t over s.
|
Finset.inf_le
theorem Finset.inf_le :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {f : β → α} {b : β},
b ∈ s → s.inf f ≤ f b
This theorem, `Finset.inf_le`, states that for any types `α` and `β`, under the conditions that `α` forms a semilattice with an infimum operation and has a top element, given a finite set `s` of elements of type `β`, a function `f` from `β` to `α`, and an element `b` of type `β`, if `b` is an element of `s`, then the infimum of the set of values obtained by applying `f` to each element of `s` is less than or equal to `f(b)`. In mathematical terms, given a set $S \subseteq \beta$ and a function $f: \beta \rightarrow \alpha$, if $b \in S$, then $\inf_{x \in S} f(x) \leq f(b)$.
More concisely: For any semilattice `α` with top element, and given a finite set `S` of elements in type `β` and a function `f` from `β` to `α`, if `b` is an element of `S`, then the infimum of `f` over `S` is less than or equal to `f(b)`.
|
iSup_eq_iSup_finset'
theorem iSup_eq_iSup_finset' :
∀ {α : Type u_2} {ι' : Sort u_7} [inst : CompleteLattice α] (s : ι' → α), ⨆ i, s i = ⨆ t, ⨆ i ∈ t, s i.down := by
sorry
This theorem states that, given a function `s` mapping from some arbitrary type `ι'` (which could be either a proper type or a proposition) to a complete lattice `α`, the supremum (i.e., least upper bound) of `s i` taken over all `i` is equal to the supremum of suprema taken over all finite subsets `t` of `ι'`, where each `t` is subjected to the condition `i ∈ t`. This general version works for all sorts `ι'`, whereas the variant `iSup_eq_iSup_finset` works for proper types only, but does not require lifting propositions to types. Here, `down` is used to convert a propositionally lifted type back to its corresponding proposition.
More concisely: Given a function from an arbitrary type or proposition `ι'` to a complete lattice `α`, the supremum of `s i` over all `i` in `ι'` equals the supremum of the suprema of `s i` over all finite subsets `t` of `ι'` where `i` is in `t`.
|
Finset.sup_cons
theorem Finset.sup_cons :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {b : β}
(h : b ∉ s), (Finset.cons b s h).sup f = f b ⊔ s.sup f
This theorem, `Finset.sup_cons`, states that for any types `α` and `β`, given a semilattice sup structure and order bot structure on `α`, a finite set `s` of type `β`, a function `f` mapping from `β` to `α`, and an element `b` of type `β` not in `s`, the supremum of the set obtained by adding `b` to `s` applied under `f` is equal to the supremum of `f` applied to `b` and the supremum of the set `s` under `f`. In mathematical terms, `sup {b} ∪ s f = f b ⊔ sup s f`.
More concisely: For any semilattice sup and order bot structures on type `α`, given a finite set `s` of type `β`, a function `f` from `β` to `α`, and an element `b` not in `s`, the supremum of `f` applied to `b` and the set `s` under `f` is equal to the supremum of the set obtained by adding `b` to `s` applied under `f`. In symbols: `sup (b :: s) f = sup s f ⊔ f b`.
|
Set.iInter_eq_iInter_finset
theorem Set.iInter_eq_iInter_finset : ∀ {α : Type u_2} {ι : Type u_5} (s : ι → Set α), ⋂ i, s i = ⋂ t, ⋂ i ∈ t, s i
This theorem states that for any type `α` and `ι`, and for any indexed family of sets `s : ι → Set α`, the intersection of all sets in this family is equal to the intersection of all intersections of finite subfamilies of this family. In other words, it implies that you can generate the intersection of an entire collection of sets by taking the intersections of all possible finite subcollections. This version of the theorem assumes `ι` to be a type, and there is another variation of the theorem `iInter_eq_iInter_finset'` that works when `ι` is a sort.
More concisely: For any indexed family of sets `s : ι → Set α`, the intersections of all sets in the family and of all finite subfamilies are equal: `∩ₙ i, s i = ∩ₙ J ∈ Finset.subsets ι, ∧ j ∈ J, ∩ₘ i ∈ J, s i`.
|
Finset.iSup_union
theorem Finset.iSup_union :
∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] [inst_1 : DecidableEq α] {f : α → β} {s t : Finset α},
⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x
The theorem `Finset.iSup_union` states that for all types `α` and `β` where `β` is a Complete Lattice and `α` has decidable equality, for any function `f` from `α` to `β` and any finite sets `s` and `t` of type `α`, the supremum of `f(x)` for `x` in the union of `s` and `t` is equal to the join (supremum in the lattice structure) of the supremum of `f(x)` for `x` in `s` and the supremum of `f(x)` for `x` in `t`. This theorem essentially says that the supremum operation distributes over the union of sets in this context.
More concisely: For any Complete Lattice β and type α with decidable equality, the supremum of a function from α to β over the union of two finite sets is equal to the join of the supremums over each set.
|
Finset.exists_nat_subset_range
theorem Finset.exists_nat_subset_range : ∀ (s : Finset ℕ), ∃ n, s ⊆ Finset.range n
The theorem `Finset.exists_nat_subset_range` states that for every finite set `s` of natural numbers, there exists a natural number `n` such that `s` is a subset of the set of natural numbers less than `n`. In other words, you can always find a number `n` such that all elements of the finite set `s` are less than `n`.
More concisely: For every finite set of natural numbers, there exists a natural number that is an upper bound for the set.
|
Finset.sup_comm
theorem Finset.sup_comm :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β)
(t : Finset γ) (f : β → γ → α), (s.sup fun b => t.sup (f b)) = t.sup fun c => s.sup fun b => f b c
This theorem states that for any types `α`, `β`, and `γ`, and given that `α` is a semilattice with a least element `⊥`, the supremum of a function `f` applied to elements of two finite sets `s` and `t` is commutative. In other words, calculating the supremum over set `s` and then over set `t` is the same as calculating the supremum over set `t` and then over set `s`. Specifically, given a function `f` from `β` and `γ` to `α`, `(Finset.sup s fun b => Finset.sup t (f b))` equals to `(Finset.sup t fun c => Finset.sup s fun b => f b c)`.
More concisely: For any semilattice `α` with least element `⊥`, and given finite sets `s` and `t`, the supremum of a function `f` applied to elements of `s` and then to `t` is equal to the supremum of the same function first applied to `t` and then to `s`. In other words, `Finset.sup s (λb, Finset.sup t (λc, f b c))` equals `Finset.sup t (λc, Finset.sup s (λb, f b c))`.
|
Finset.sup'_le
theorem Finset.sup'_le :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α},
(∀ b ∈ s, f b ≤ a) → s.sup' H f ≤ a
The theorem `Finset.sup'_le` is an alias of the reverse direction of `Finset.sup'_le_iff`. It states that for any types `α` and `β` where `α` forms a join-semilattice, if we are given a nonempty finite set `s` of type `β`, a function `f` from `β` to `α`, and an element `a` of type `α`, if every element `b` in the finite set `s` satisfies the condition that `f(b)` is less than or equal to `a`, then the supremum of the image of `s` under `f` is less than or equal to `a`. This supremum is computed by the function `Finset.sup'` and it represents the greatest lower bound of the set `{f(b) | b ∈ s}`.
More concisely: If `α` is a join-semilattice, `s` is a nonempty finite set of type `β`, `f` is a function from `β` to `α`, and `a` is an element of `α` such that `f(b) ≤ a` for all `b` in `s`, then `Finset.sup' s f ≤ a`.
|
Finset.sup'_le_iff
theorem Finset.sup'_le_iff :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α},
s.sup' H f ≤ a ↔ ∀ b ∈ s, f b ≤ a
The theorem `Finset.sup'_le_iff` asserts that for any types `α` and `β`, given a semilattice structure on `α`, a nonempty finset `s` of elements of type `β`, a function `f` from `β` to `α`, and an element `a` of type `α`, the supremum of the images of elements of `s` under `f` is less than or equal to `a` if and only if every element `b` of `s` satisfies that its image under `f` is less than or equal to `a`. This essentially means that the supremum of the images under `f` is the smallest upper bound for all such images.
More concisely: For any semilattice `α`, nonempty finset `s` of elements `β`, function `f` from `β` to `α`, and `a` in `α`, the image supremum of `s` under `f` is less than or equal to `a` if and only if the image of every element in `s` under `f` is less than or equal to `a`.
|
Finset.sup_inf_distrib_right
theorem Finset.sup_inf_distrib_right :
∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] [inst_1 : OrderBot α] (s : Finset ι) (f : ι → α) (a : α),
s.sup f ⊓ a = s.sup fun i => f i ⊓ a
This theorem, named `Finset.sup_inf_distrib_right`, states that for any type `α` which forms a distributive lattice and also has a bottom element, any finite set `s` of elements of type `ι`, any function `f` from `ι` to `α`, and any element `a` of type `α`, the supremum (greatest element) of the image of `s` under `f`, intersected with `a`, is equal to the supremum of the image of `s` under the function that maps each element of `s` to its image under `f` intersected with `a`. In mathematical terms, it asserts that the operation of taking the supremum of a set and intersecting with an element distributes over the elements of the set: $\bigvee_{i \in s} f(i) \wedge a = \bigvee_{i \in s} (f(i) \wedge a)$.
More concisely: For any distributive lattice `α` with bottom element and finite set `s` from index type `ι`, the supremum of images of `s` under `f` intersected with an element `a` is equal to the supremum of images of `s` under the function that maps each element to its intersection with `a`. In other words, $\bigvee_{i \in s} (f(i) \wedge a) = \bigvee_{i \in s} f(i) \wedge a$.
|
Set.iUnion_eq_iUnion_finset
theorem Set.iUnion_eq_iUnion_finset : ∀ {α : Type u_2} {ι : Type u_5} (s : ι → Set α), ⋃ i, s i = ⋃ t, ⋃ i ∈ t, s i
The theorem `Set.iUnion_eq_iUnion_finset` states that for any type `α` and any index type `ι`, the union of an indexed family of sets `s : ι → Set α` is equivalent to the union of the unions of finite subfamilies of `ι`. In other words, it states that taking the union over all sets indexed by `ι` is the same as taking the union over all finite subsets of `ι`, and then taking the union over all sets indexed by elements in these subsets. This version of the theorem assumes `ι : Type*`. There is a similar version of this theorem, `iUnion_eq_iUnion_finset'`, that works for `ι : Sort*`.
More concisely: For any type `α` and index type `ι:*`, the indexed union of sets `s : ι → Set α` equals the union of unions of finite subsets of `ι` over their elements.
|
Finset.disjoint_sup_right
theorem Finset.disjoint_sup_right :
∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α} {a : α},
Disjoint a (s.sup f) ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint a (f i)
The theorem `Finset.disjoint_sup_right` states that for any types `α` and `ι`, any distributive lattice structure on `α` with a least element, any finite set `s` of type `ι`, any function `f` from `ι` to `α`, and any element `a` of `α`, the element `a` is disjoint from the supremum of the set `s` under `f` if and only if `a` is disjoint from `f i` for every element `i` in `s`. Here, two elements of a lattice are defined to be disjoint if their infimum is the bottom element. The supremum of a finite set `s` under `f` is the result of applying the binary operation (supremum) to each element of `s` in turn, starting from the least element of the lattice.
More concisely: For any distributive lattice with least element, an element is disjoint from the supremum of a finite set under a function if and only if it is disjoint from the image of each element in the set.
|
Mathlib.Data.Finset.Lattice._auxLemma.5
theorem Mathlib.Data.Finset.Lattice._auxLemma.5 : ∀ {a b c : Prop}, (a ∨ b → c) = ((a → c) ∧ (b → c))
This theorem, `Mathlib.Data.Finset.Lattice._auxLemma.5`, states that for any three propositions `a`, `b`, and `c`, the proposition that `c` is implied by either `a` or `b` (`a ∨ b → c`) is equivalent to the proposition that `c` is implied by `a` and `c` is implied by `b` (`(a → c) ∧ (b → c)`). In other words, if `c` follows from either `a` or `b`, then it must follow from `a` and it must also follow from `b`.
More concisely: The proposition `(a ∨ b) → c` is logically equivalent to `(a → c) ∧ (b → c)`.
|
Finset.min'_mem
theorem Finset.min'_mem : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty), s.min' H ∈ s := by
sorry
This theorem states that for any given type `α` which has a linear order, and any nonempty finite set `s` of elements of that type, the minimum element of `s` (denoted by `Finset.min' s H` where `H` is a proof of nonemptiness) is indeed an element of `s`. In mathematical terms, if `s` is a nonempty finite set in a totally ordered set, the minimum element of `s` belongs to `s`.
More concisely: If `s` is a nonempty finite subset of a totally ordered set `α`, then `Finset.min s` is an element of `s`.
|
Set.iInter_eq_iInter_finset'
theorem Set.iInter_eq_iInter_finset' :
∀ {α : Type u_2} {ι' : Sort u_7} (s : ι' → Set α), ⋂ i, s i = ⋂ t, ⋂ i ∈ t, s i.down
The theorem `Set.iInter_eq_iInter_finset'` states that for any type `α` and any index `ι'`, and given a function `s` mapping from the index to a set of `α`, the intersection over all elements in the index of the sets `s i` (represented as `⋂ i, s i`) is equal to the intersection over all subsets `t` of the index of the intersections of the sets `s i` for each `i` in `t` (represented as `⋂ t, ⋂ i ∈ t, s i.down`). In other words, this theorem asserts that the intersection of an indexed family of sets is equivalent to the intersection of the intersections of finite subfamilies. This version of the theorem works for any `Sort*` as the index set `ι'`. There is another version `iInter_eq_iInter_finset` that assumes `ι'` to be `Type*`, but avoids `PLift`s in the right-hand side.
More concisely: For any type `α` and index set `ι'`, the intersection of an indexed family of sets `s i` equals the intersection of the intersections of sets `s i` over all finite subsets of `ι'`.
|
Finset.induction_on_max_value
theorem Finset.induction_on_max_value :
∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : DecidableEq ι] (f : ι → α) {p : Finset ι → Prop}
(s : Finset ι), p ∅ → (∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → p s → p (insert a s)) → p s
The theorem `Finset.induction_on_max_value` is an induction principle for finite sets (`Finset`s) in any type, provided we have a function `f` that maps to a linearly ordered type. The theorem states that a property `p` holds for all finite sets `s` of type `ι` if the following conditions are met:
- The property `p` holds for the empty finite set.
- For any finite set `s` and an element `a` not in `s`, if for all elements `x` in `s` the value `f(x)` is less than or equal to `f(a)`, then the property `p` being true for `s` implies that `p` is also true for the finite set obtained by inserting `a` into `s`.
This can be seen as an induction over the maximum value of the function `f` on the elements of the finite set.
More concisely: Given a linearly ordered type ι and a property p, if p holds for the empty set and for all x ∈ s with f(x) ≤ f(a), p(s) implies p(s ∪ {a}), then p holds for all finite sets s of type ι.
|
Finset.max'_eq_sup'
theorem Finset.max'_eq_sup' :
∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty), s.max' H = s.sup' H id
This theorem states that for any nonempty finite set `s` of a given type `α` under a linear order, the maximum element of `s` (given by `Finset.max' s H` where `H` is a proof of the set's non-emptiness) is equal to the supremum of its image under the identity function (given by `Finset.sup' s H id`). In other words, in a linearly ordered set, the maximum element is the same as the supremum when considering the identity function.
More concisely: For any nonempty finite set `s` under a linear order, the maximum element is equal to the supremum of its elements under the identity function.
|
Finset.inf_insert
theorem Finset.inf_insert :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {f : β → α}
[inst_2 : DecidableEq β] {b : β}, (insert b s).inf f = f b ⊓ s.inf f
The theorem `Finset.inf_insert` asserts that for any semilattice with top (`SemilatticeInf` and `OrderTop`), any finite set (`Finset`) `s` of type `β`, any function `f` from `β` to `α`, and any element `b` of `β`, the infimum (greatest lower bound) of the set obtained by applying `f` to each element of the set `s` with `b` inserted (`insert b s`), is equal to the infimum of `f(b)` and the infimum of the set obtained by applying `f` to each element of `s`. This is true when equality for elements of `β` is decidable (`DecidableEq β`). In mathematical terms, this can be written as `inf(f(b ∪ s)) = f(b) ⊓ inf(f(s))`.
More concisely: For any semilattice with top, finite set, function, and decidable equality, the infimum of the function applied to each element of the set with a new element inserted is equal to the infimum of the function applied to the new element and the infimum of the function applied to each element of the set. (Mathematically: `inf(f(b ∪ s)) = f(b) ∧ inf(f(s))`)
|
Finset.card_le_of_interleaved
theorem Finset.card_le_of_interleaved :
∀ {α : Type u_2} [inst : LinearOrder α] {s t : Finset α},
(∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y) → s.card ≤ t.card + 1
The theorem states that for any two finite sets `s` and `t` of a type `α` that has a linear order, if for every pair of distinct elements `x` and `y` in `s` with `x < y`, it holds that there is no other element from `s` strictly between `x` and `y`, and there exists an element `z` in `t` that is strictly between `x` and `y`, then the cardinality of `s` is less than or equal to the cardinality of `t` plus one. In other words, if `s` and `t` are interleaved with `t` filling the gaps between elements of `s`, then the number of elements in `s` is at most the number of elements in `t` plus one.
More concisely: If two finite linear ordered sets `s` and `t` satisfy the condition that for every pair of distinct elements `x` and `y` in `s` with `x < y`, there is no element from `s` strictly between `x` and `y`, but there exists an element `z` in `t` strictly between `x` and `y`, then the cardinality of `s` is less than or equal to the cardinality of `t` plus one.
|
Mathlib.Data.Finset.Lattice._auxLemma.6
theorem Mathlib.Data.Finset.Lattice._auxLemma.6 :
∀ {α : Sort u_1} {p q : α → Prop}, (∀ (x : α), p x ∧ q x) = ((∀ (x : α), p x) ∧ ∀ (x : α), q x)
This theorem, named `Mathlib.Data.Finset.Lattice._auxLemma.6`, asserts that for any type `α` and for any two properties `p` and `q` of elements of type `α`, the property of each element satisfying both `p` and `q` is equivalent to the property of each element satisfying `p` and each element satisfying `q`. In mathematical terms, this theorem states that $\forall x \in \alpha, (p(x) \land q(x))$ is equivalent to $(\forall x \in \alpha, p(x)) \land (\forall x \in \alpha, q(x))$.
More concisely: The theorem asserts that for any type `α` and properties `p` and `q` of its elements, the element-wise conjunction `p ∧ q` is equivalent to the conjunction of the sets of elements satisfying `p` and `q`, i.e., `{x | p(x)} ∧ {x | q(x)}`.
|
Finset.inf_coe
theorem Finset.inf_coe :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {P : α → Prop} {Ptop : P ⊤}
{Pinf : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)} (t : Finset β) (f : β → { x // P x }),
↑(t.inf f) = t.inf fun x => ↑(f x)
This theorem states that for any finite set `t` of elements of type `β` and any function `f` mapping elements of `β` to a subtype of `α` that is closed under the infimum operation, the infimum of the images under `f` computed in the subtype is the same as the infimum computed in `α`. Here, `α` is assumed to be a semilattice with respect to the infimum operation and also is equipped with a top element. The closure conditions are that the top element of `α` belongs to the subtype and for any two elements in the subtype, their infimum also belongs to the subtype.
More concisely: For any finite subset `t` of a semilattice `β` with top element and any function `f : β -> α` mapping `β` to a subtype of `α` closed under infimum, the infimum of `f``(t)` in `α` equals the infimum in the subtype.
|
Finset.sup'_comp_eq_image
theorem Finset.sup'_comp_eq_image :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : DecidableEq β] {s : Finset γ}
{f : γ → β} (hs : s.Nonempty) (g : β → α), s.sup' hs (g ∘ f) = (Finset.image f s).sup' ⋯ g
The theorem `Finset.sup'_comp_eq_image` is about the supremum of the composition of two functions `g` and `f` over a non-empty finite set `s`. Specifically, for any types `α`, `β`, and `γ`, where `α` forms a semilattice with a supremum operation and `β` has decidable equality, given a non-empty finite set `s` of type `γ`, a function `f` from `γ` to `β`, and a function `g` from `β` to `α`, the supremum of the composition `(g ∘ f)` over `s` is equal to the supremum of `g` over the image of `s` under `f`. That is, applying `g ∘ f` to each element of `s` and taking the supremum gives the same result as first applying `f` to each element of `s`, forming a new set, and then applying `g` to each element of this new set and taking the supremum.
More concisely: For any semilattice α with decidable equality, non-empty finite set s of type γ, functions f : γ -> β and g : β -> α, the supremum of g ∘ f over s equals the supremum of g over the image of s under f.
|
Finset.card_le_diff_of_interleaved
theorem Finset.card_le_diff_of_interleaved :
∀ {α : Type u_2} [inst : LinearOrder α] {s t : Finset α},
(∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y) → s.card ≤ (t \ s).card + 1
The theorem `Finset.card_le_diff_of_interleaved` states that for any two finite sets `s` and `t` over a type `α` that has a linear order, if the elements of `s` are interleaved within `t` (meaning that for every two distinct elements `x` and `y` in `s` where `x < y`, there is an element `z` in `t` such that `x < z < y` and there are no other elements of `s` in the open interval between `x` and `y`), then the cardinality of `s` is less than or equal to the cardinality of the difference set of `t` and `s` (i.e., elements that are in `t` but not in `s`) plus one.
More concisely: If sets `s` and `t` over a linearly ordered type have no elements from `s` in the open intervals between distinct elements of `s`, then `|s| ≤ |t \ s| + 1`.
|
Finset.sup'_eq_sup
theorem Finset.sup'_eq_sup :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} (H : s.Nonempty)
(f : β → α), s.sup' H f = s.sup f
The theorem `Finset.sup'_eq_sup` states that for any types `α` and `β`, where `α` is a join-semilattice and also has a bottom element, any nonempty finite set `s` of type `β`, and any function `f` from `β` to `α`, the supremum of the image of `s` under `f` calculated with `Finset.sup'` (which requires a proof of non-emptiness of `s`) is equal to the supremum calculated with `Finset.sup` (which does not require `s` to be nonempty due to presence of a bottom element in `α`). In other words, if `s` is not empty, these two methods for calculating the supremum of the image of `s` under `f` are equivalent.
More concisely: For any join-semilattice `α` with a bottom element, nonempty finite set `s` of type `β`, and function `f` from `β` to `α`, `Finset.sup' (f '' s) = Finset.sup (f '' s)`.
|
Finset.coe_sup'
theorem Finset.coe_sup' :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α),
↑(s.sup' H f) = s.sup (WithBot.some ∘ f)
This theorem states that for any types `α` and `β`, where `α` forms a join-semilattice, and for any nonempty finite set `s` of type `β`, as well as any function `f` from `β` to `α`, the supremum of the image of `s` under `f` when taken as an element of the extended type `WithBot α`, is equal to the supremum of the image under `f` composed with the canonical map from `α` to `WithBot α`. In other words, `↑(Finset.sup' s H f)` (the coercive map of the supremum of the image of `s` under `f` to `WithBot α`) equals `Finset.sup s (WithBot.some ∘ f)` (the supremum of the image under `f` composed with the canonical embedding to `WithBot α`). This establishes the commutativity between the supremum operation and the canonical embedding function in this context.
More concisely: For any join-semilattice `α`, function `f` from type `β` to `α`, and nonempty finite set `s` of type `β`, the supremum of `f` applied to `s` in the extended type `WithBot α` equals the supremum of `f`(x) for all x in `s`, composed with the canonical map from `α` to `WithBot α`.
|
Finset.induction_on_min_value
theorem Finset.induction_on_min_value :
∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : DecidableEq ι] (f : ι → α) {p : Finset ι → Prop}
(s : Finset ι), p ∅ → (∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f a ≤ f x) → p s → p (insert a s)) → p s
The theorem, `Finset.induction_on_min_value`, is an induction principle for finite sets (`Finset`s) in any type from which a given function `f` maps to a linearly ordered type. This principle asserts that a predicate is true for all finite sets in said type if it satisfies the following two conditions:
* The predicate is true for the empty finite set.
* For any finite set `s` and an element `a` not in `s` where `f a` is less than or equal to `f x` for all `x` in `s`, if the predicate is true for `s`, then it is also true for the set that results from inserting `a` into `s`.
The theorem requires `f` to map from any type `ι` to a linearly ordered type `α`. Additionally, it assumes that equality in `ι` is decidable.
More concisely: If `f : ι -> α` maps any type `ι` to a linearly ordered type `α` with decidable equality, then a predicate holds for all finite sets `s` in `ι` if it holds for the empty set and is preserved under adding an element `a not in s` with `f a <= f x` for all `x in s`.
|
iSup_eq_iSup_finset
theorem iSup_eq_iSup_finset :
∀ {α : Type u_2} {ι : Type u_5} [inst : CompleteLattice α] (s : ι → α), ⨆ i, s i = ⨆ t, ⨆ i ∈ t, s i
This theorem states that for any types `α` and `ι` with `α` being a complete lattice, and any function `s` from `ι` to `α`, the supremum of `s i` over all `i` in `ι` is equal to the supremum over all finite subsets `t` of `ι` of the suprema of `s i` for `i` in `t`. In other words, we can find the supremum of the range of a function `s` by taking the supremum of the suprema over all finite subsets of its domain.
More concisely: For any complete lattice `α` and any function `s` from a index set `ι` to `α`, the supremum of `s i` over all `i` in `ι` equals the supremum over all finite subsets `t` of `ι` of the suprema of `s i` for `i` in `t`. Equivalently, the supremum of `s` is the supremum of the finite suprema of `s` over all finite subsets of its domain.
|
Monotone.map_finset_min'
theorem Monotone.map_finset_min' :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
Monotone f → ∀ {s : Finset α} (h : s.Nonempty), f (s.min' h) = (Finset.image f s).min' ⋯
This theorem asserts that for any given types `α` and `β` equipped with a linear order, and given a function `f` from `α` to `β` that is monotonic, if we have a nonempty `Finset` `s` of type `α`, then the minimum element of the image of `s` under `f` is the image of the minimum element of `s` under `f`. In other words, if `f` is a monotonic function, it preserves the minimum element when mapping a nonempty finite set from one ordered set to another.
More concisely: If `f` is a monotonic function between ordered sets `α` and `β`, then the image of the minimum element of any nonempty finite subset `s` of `α` under `f` is the minimum element of `f``(s)`.
|
Finset.sup_biUnion
theorem Finset.sup_biUnion :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α}
[inst_2 : DecidableEq β] (s : Finset γ) (t : γ → Finset β), (s.biUnion t).sup f = s.sup fun x => (t x).sup f
The theorem `Finset.sup_biUnion` states that for all types `α`, `β`, and `γ` with `α` being a semilattice with least element (`OrderBot α`), given a function `f` from `β` to `α`, a decision procedure for equality of `β` elements (`DecidableEq β`), a finite set `s` of elements of type `γ`, and a function `t` from `γ` to finite sets of `β`, then the supremum (greatest element) of the union of all `t x` (for each `x` in `s`) under the function `f` is equal to the supremum of the set `s` under the function which maps `x` to the supremum of `t x` under `f`. In other words, we can either first form the union of all sets `t x` and then find the supremum, or we can first find the supremum of each `t x` and then find the supremum of these supremums, and the result will be the same. This is a property of the function `sup` applied to the union of finite sets in the context of semilattices.
More concisely: For any semilattice `α` with least element, given a function `f : β -> α`, a decision procedure for equality of `β`, a finite set `s : γ`, and a function `t : γ -> Finset β`, the supremum of `f` applied to the union of `t x` for all `x` in `s` equals the supremum of `f` applied to the supremum of each `t x`.
|
Finset.lt_max'_of_mem_erase_max'
theorem Finset.lt_max'_of_mem_erase_max' :
∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty) [inst_1 : DecidableEq α] {a : α},
a ∈ s.erase (s.max' H) → a < s.max' H
The theorem `Finset.lt_max'_of_mem_erase_max'` states that for any nonempty finite set `s` of a type `α` that is ordered by a linear order, along with a provided instance of decidable equality on `α`, if an element `a` belongs to the set resulting from erasing the maximum element of `s` from `s` itself, then `a` is strictly less than the maximum element of `s`. In other words, any element of the set excluding its maximum is less than the maximum.
More concisely: For any nonempty finite set `s` in a linearly ordered type `α` with decidable equality, if `a` is an element of `s` excluding its maximum, then `a` is strictly less than the maximum element of `s`.
|
iInf_eq_iInf_finset
theorem iInf_eq_iInf_finset :
∀ {α : Type u_2} {ι : Type u_5} [inst : CompleteLattice α] (s : ι → α), ⨅ i, s i = ⨅ t, ⨅ i ∈ t, s i
The theorem `iInf_eq_iInf_finset` states that for any type `α` that forms a complete lattice, and any function `s` from some type `ι` to `α`, the infimum (greatest lower bound) of the set of all `s i` for `i` in `ι` is the same as the infimum of the set of all infima `⨅ i ∈ t, s i` for `t` a finite subset of `ι`. This version of the theorem assumes that `ι` is a type. There is another version called `iInf_eq_iInf_finset'` that works for `ι` being any sort.
More concisely: For any complete lattice α and function s from type ι to α, the infimum of {si : i ∈ ι} equals the infimum of {⨅ i ∈ t, si : t finite subset of ι}.
|
Finset.sup_empty
theorem Finset.sup_empty :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α}, ∅.sup f = ⊥
This theorem, `Finset.sup_empty`, states that for any types `α` and `β`, given a semilattice (a partially ordered set with a supremum operation) and a least element (`OrderBot`) on `α`, and any function `f` from `β` to `α`, then the supremum of `f` over an empty set is the least element of `α`. In more mathematical terms, this is saying that the supremum of an empty set under any function is the bottom element of the semilattice.
More concisely: For any semilattice with least element and function from a type to it, the supremum of the empty set under that function equals the least element.
|
map_finset_sup
theorem map_finset_sup :
∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [inst : SemilatticeSup α] [inst_1 : OrderBot α]
[inst_2 : SemilatticeSup β] [inst_3 : OrderBot β] [inst_4 : FunLike F α β] [inst_5 : SupBotHomClass F α β] (f : F)
(s : Finset ι) (g : ι → α), f (s.sup g) = s.sup (⇑f ∘ g)
The theorem `map_finset_sup` states that for all types `F`, `α`, `β`, and `ι`, given instances of `SemilatticeSup` and `OrderBot` for `α` and `β`, an injective function-like instance `FunLike F α β`, and a instance of `SupBotHomClass F α β` (which indicates that `F` is a function that preserves suprema and bottom elements), along with a function `f` of type `F`, a finite set `s` of type `Finset ι`, and a function `g` from `ι` to `α`, the supremum of the mapping of `f` over the set `s` after applying `g` (`f (Finset.sup s g)`) is the same as the supremum of the set `s` after applying the composition of `f` and `g` (`Finset.sup s (⇑f ∘ g)`).
In other words, the function `f` can be "pushed through" the `sup` operation, demonstrating a distributive property of `f` over the `sup` operation for finite sets.
More concisely: For any type `F`, `α`, `β`, and `ι`, given instances of `SemilatticeSup` and `OrderBot` for `α` and `β`, an injective `FunLike F α β`, and a `SupBotHomClass F α β`, the application of `f ∘ g` to the supremum of a finite set `s` is equal to the supremum of the image of `f` over the set `s` after applying `g`.
|
Finset.sup_image
theorem Finset.sup_image :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : OrderBot α]
[inst_2 : DecidableEq β] (s : Finset γ) (f : γ → β) (g : β → α), (Finset.image f s).sup g = s.sup (g ∘ f)
The theorem `Finset.sup_image` states that for any types `α`, `β`, and `γ`, given a semi-lattice structure and a bottom element on `α`, and a decidable equality on `β`, for any finite set `s` of type `γ`, a function `f` from `γ` to `β`, and a function `g` from `β` to `α`, the supremum of the image of `s` under `f` with respect to `g` is equal to the supremum of `s` with respect to the composition of `g` and `f`. In other words, we can either take the supremum after applying the function `f` or we can take the supremum first and then apply the function `f`; both ways will give us the same result.
More concisely: For any semi-lattice `α` with bottom element, decidable equality on `β`, finite set `s` of type `γ`, functions `f: γ -> β` and `g: β -> α`, the image of `s` under `f` supremum-mapped by `g` equals the supremum of `s` supremum-mapped by the composition `g ∘ f`.
|
Finset.sup_eq_biUnion
theorem Finset.sup_eq_biUnion :
∀ {α : Type u_7} {β : Type u_8} [inst : DecidableEq β] (s : Finset α) (t : α → Finset β), s.sup t = s.biUnion t
The theorem `Finset.sup_eq_biUnion` asserts that for any two types `α` and `β` with `β` having a decidable equality relation, and for any finite set `s` of type `α` and a function `t` mapping an element of `α` to a finite set of `β`, the supremum of the set `s` under the function `t` is equal to the biUnion of `s` and `t`. In other words, if you take a finite set and map each element to another finite set via a function, the supremum of the original set under this function is the same as if you had taken the union of the function's outputs for all elements in the original set.
More concisely: For any decidably equated types `α` and `β`, given a finite set `s` of `α` and a function `t` mapping each `α` element to a finite set of `β`, the supremum of `s` under `t` equals the biUnion of the image of `s` under `t`.
|
Finset.prodMk_sup'_sup'
theorem Finset.prodMk_sup'_sup' :
∀ {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β]
{s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β),
(s.sup' hs f, t.sup' ht g) = (s ×ˢ t).sup' ⋯ (Prod.map f g)
The theorem `Finset.prodMk_sup'_sup'` states that for any two nonempty finite sets `s` and `t` of types `ι` and `κ` respectively, and any two functions `f : ι → α` and `g : κ → β`, where `α` and `β` are types equipped with a semilattice structure (that is, a structure where elements can be combined using a 'sup' operation satisfying certain properties), the pair `(s.sup' hs f, t.sup' ht g)`, where `s.sup' hs f` and `t.sup' ht g` represent the supremum (i.e., the least upper bound) of the image of `s` and `t` under `f` and `g` respectively, is equal to the supremum of the images of the Cartesian product of `s` and `t` under the function `Prod.map f g`. Here, `Prod.map f g` is a function that applies `f` to the first component and `g` to the second component of a pair (from the Cartesian product of `s` and `t`).
More concisely: For any nonempty finite sets `s` of type `ι` and `t` of type `κ`, and functions `f : ι → α` and `g : κ → β` from types equipped with a semilattice structure, the supremum of the images of `s` and `t` under `f` and `g` respectively, is equal to the supremum of the images of their Cartesian product under `Prod.map f g`.
|
Finset.sup_le
theorem Finset.sup_le :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {a : α},
(∀ b ∈ s, f b ≤ a) → s.sup f ≤ a
The theorem `Finset.sup_le` in Lean 4 states that for any types `α` and `β`, given a semi lattice `α` with a least element, a finite set `s` of elements of type `β`, a function `f` from `β` to `α`, and an element `a` of type `α`, if for all elements `b` in the set `s`, the image of `b` under `f` is less than or equal to `a`, then the supremum of the set `s` under the function `f` is also less than or equal to `a`. This theorem is an alias of the converse implication of `Finset.sup_le_iff`.
More concisely: If `α` is a semi-lattice with a least element, `s` is a finite set of elements from type `β`, `f` is a function from `β` to `α`, and for all `b` in `s`, `f(b) ≤ a`, then `sup(s : β → α) ≤ a` in `α`.
|
Finset.mem_of_max
theorem Finset.mem_of_max : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α} {a : α}, s.max = ↑a → a ∈ s := by
sorry
The theorem `Finset.mem_of_max` states that for any type `α` equipped with a linear order and for any finite set `s` of type `α` and any element `a` of type `α`, if the maximum element of the set `s` is `a` (i.e., `Finset.max s = ↑a`), then `a` is an element of `s`. This theorem essentially asserts the basic property that if `a` is the maximum element in a finite set, then `a` must necessarily be in the set.
More concisely: If a finite set `s` has maximum element `a`, then `a` is an element of `s`.
|
Finset.sup_lt_iff
theorem Finset.sup_lt_iff :
∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α} {a : α},
⊥ < a → (s.sup f < a ↔ ∀ b ∈ s, f b < a)
The theorem `Finset.sup_lt_iff` states that for any types `α` and `ι`, given a linear order on `α`, a minimum element (or bottom) for `α`, a finite set `s` of type `ι`, a function `f` mapping `ι` to `α`, and an element `a` of `α` such that the minimum element is less than `a`, the supremum of the set `s` under the function `f` is less than `a` if and only if for all elements `b` in `s`, the value of the function `f` at `b` is less than `a`. In mathematical terms, it shows the condition under which the supremum of a set is less than a certain value.
More concisely: For any linear order on a type `α`, a minimum element `⊥` in `α`, a finite set `s` of type `ι`, a function `f : ι → α`, and `a ∈ α` with `⊥ < a`, if for all `b ∈ s`, we have `f b < a`, then `sup (f '' s) < a`.
|
Finset.sup_mono_fun
theorem Finset.sup_mono_fun :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f g : β → α},
(∀ b ∈ s, f b ≤ g b) → s.sup f ≤ s.sup g
The theorem `Finset.sup_mono_fun` states that for all types `α` and `β`, where `α` is a semilattice sup and an order bot, and given a finite set `s` of type `β`, and two functions `f` and `g` from `β` to `α`, if every element `b` in the set `s` meets the condition that `f(b)` is less than or equal to `g(b)`, then the supremum of the set `s` under the function `f` is less than or equal to the supremum of the set `s` under the function `g`. In simple terms, if a function `f` is pointwise less than or equal to a function `g` for all elements in a set, then the maximum value of `f` over the set is less than or equal to the maximum value of `g` over the same set.
More concisely: If `f` is pointwise less than or equal to `g` for all elements in a finite set `s`, then the supremum of `s` under `f` is less than or equal to the supremum of `s` under `g`.
|
Finset.max_of_nonempty
theorem Finset.max_of_nonempty : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α}, s.Nonempty → ∃ a, s.max = ↑a
The theorem `Finset.max_of_nonempty` states that for any type `α` which has a linear order, and for any finite set `s` of this type, if `s` is nonempty, then there exists an element `a` such that the maximum of the set `s` is `a`. The maximum of a set is defined as the largest element in the set according to the given linear order.
More concisely: For any linear order type `α` and finite nonempty set `s` of `α`, there exists an element `a` in `s` such that `s ≤ a` for all `x` in `s`. (Here, `≤` denotes the linear order relation.)
|
Finset.sup'_cons
theorem Finset.sup'_cons :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {b : β}
{hb : b ∉ s}, (Finset.cons b s hb).sup' ⋯ f = f b ⊔ s.sup' H f
The theorem `Finset.sup'_cons` states that for any types `α` and `β` with `α` being a join-semilattice, any nonempty finite set `s` of type `β`, any function `f` from `β` to `α`, and any element `b` of `β` not belonging to `s`, the supremum of the image under `f` of the set created by adding `b` to `s` is the supremum of `f(b)` and the supremum of the image under `f` of `s`. In mathematical terms, if we consider `f` as a function mapping elements of `s` to a join-semilattice `α`, then the supremum of the image of `s ∪ {b}` under `f` is equal to `f(b) ⊔ sup(f(s))`, where `⊔` is the join operation in the semilattice.
More concisely: For any join-semilattice `α`, function `f` from a nonempty finite set `s` in `β` to `α`, and element `b` not in `s`, the supremum of `f(s ∪ {b})` equals the join of `f(b)` and the supremum of `f(s)`.
|
Finset.inf_cons
theorem Finset.inf_cons :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {f : β → α} {b : β}
(h : b ∉ s), (Finset.cons b s h).inf f = f b ⊓ s.inf f
The theorem `Finset.inf_cons` states that for any types `α` and `β`, given an instance of the semilattice structure for `α`, an order-top structure for `α`, a finite set `s` of type `β`, a function `f` from `β` to `α`, and an element `b` of type `β` which is not in `s`, the infimum of the union of `{b}` and `s` (i.e., `Finset.cons b s h`) under the function `f` is equal to the infimum of `f` at `b` and the infimum of `s` under `f`. In mathematical terms, this says that $\inf \{f(b)\} \cup \inf \{f(s)\} = f(b) \land \inf \{f(s)\} $, where $\land$ represents the infimum (or greatest lower bound) operation in the semilattice.
More concisely: For any semilattice and order-topped type `α`, finite set `s` of type `β`, function `f` from `β` to `α`, and `b` not in `s`, the infimum of `f` at `b` and the infimum of `s` under `f` is equal to the infimum of `f` applied to the set `{b} ∪ s`.
|
Finset.inf'_prodMap
theorem Finset.inf'_prodMap :
∀ {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β]
{s : Finset ι} {t : Finset κ} (hst : (s ×ˢ t).Nonempty) (f : ι → α) (g : κ → β),
(s ×ˢ t).inf' hst (Prod.map f g) = (s.inf' ⋯ f, t.inf' ⋯ g)
The theorem `Finset.inf'_prodMap` states that for any types `ι`, `κ`, `α`, `β` where `α` and `β` are semilattice infimums, and for any finite sets `s` of type `ι` and `t` of type `κ`, if the Cartesian product of `s` and `t` is nonempty, then the infimum of the Cartesian product of `s` and `t` using the product map of functions `f : ι → α` and `g : κ → β` is equal to the tuple containing the infimum of `s` applying function `f` and the infimum of `t` applying function `g`.
In simpler terms, this theorem is about computing the minimum (infimum) of two sets, each of which is being transformed by a function. It says that you can first transform each set and then compute the infimum, or you can first compute a kind of combined infimum and then transform the result. It ensures that these two procedures give you the same answer.
More concisely: Given types `ι`, `κ`, `α` with `α` and `β` being semilattice infima, functions `f : ι → α` and `g : κ → β`, and finite sets `s : Fin ι` and `t : Fin κ` with nonempty product, the infimum of `f''s` under the product map is equal to the tuple of `(inf s '' f)` and `(inf t '' g)`.
|
Finset.comp_sup_eq_sup_comp
theorem Finset.comp_sup_eq_sup_comp :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : OrderBot α]
[inst_2 : SemilatticeSup γ] [inst_3 : OrderBot γ] {s : Finset β} {f : β → α} (g : α → γ),
(∀ (x y : α), g (x ⊔ y) = g x ⊔ g y) → g ⊥ = ⊥ → g (s.sup f) = s.sup (g ∘ f)
The theorem `Finset.comp_sup_eq_sup_comp` states that for any sets `α`, `β`, and `γ`, given that `α` and `γ` are semilattice supremum and have the smallest element, and given a finite set `s` of type `β` and a function `f` from `β` to `α`, along with another function `g` from `α` to `γ`, if the function `g` preserves the supremum operation and maps the smallest element of `α` to the smallest element of `γ`, then applying the function `g` to the supremum of the image of `s` under `f` is the same as first applying `g ∘ f` to `s` and then taking the supremum. In mathematical terms, it would be expressed as `g(sup(s,f)) = sup(s, g ∘ f)`.
More concisely: If `f: β → α`, `g: α → γ` preserve suprema and map the least elements respectively, then `g(sup(s, f s)) = sup(s, g ∘ f)` for any finite set `s` in `β`.
|
Finset.sup'_comp_eq_map
theorem Finset.sup'_comp_eq_map :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] {s : Finset γ} {f : γ ↪ β} (g : β → α)
(hs : s.Nonempty), s.sup' hs (g ∘ ⇑f) = (Finset.map f s).sup' ⋯ g
The theorem `Finset.sup'_comp_eq_map` asserts that for any types `α`, `β`, and `γ`, where `α` forms a semilattice with a defined supremum operation, any non-empty finite set `s` of type `γ`, any embedding `f` from `γ` to `β`, and any function `g` from `β` to `α`, the supremum of the composite function `g ∘ f` applied to `s` is equal to the supremum of `g` applied to the image of `s` under the map `f`. This theorem provides an equality between the supremum operation applied directly on the original set through a composed function and the supremum operation applied on the mapped set.
More concisely: For any semilattice `α` with supremum operation, any non-empty finite set `s` in type `γ`, any embedding `f` from `γ` to `β`, and any function `g` from `β` to `α`, the supremum of `g` composed with `f` applied to `s` equals the supremum of `g` applied to the image of `s` under `f`.
|
Finset.sup_congr
theorem Finset.sup_congr :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s₁ s₂ : Finset β} {f g : β → α},
s₁ = s₂ → (∀ a ∈ s₂, f a = g a) → s₁.sup f = s₂.sup g
The theorem `Finset.sup_congr` asserts that for any two types `α` and `β`, where `α` is a semilattice with a least element, if we have two finite sets `s₁` and `s₂` of type `β`, and two functions `f` and `g` from `β` to `α`, if `s₁` equals `s₂` and `f a` is equal to `g a` for all `a` in `s₂`, then the supremum of `s₁` under `f` is equal to the supremum of `s₂` under `g`. In mathematical terms, this is stating that if two sets are equal and a function `f` is equal to a function `g` at every point in one of these sets, then the supremum of the set under `f` is equal to the supremum of the set under `g`.
More concisely: If `α` is a semilattice with a least element, `s₁ = s₂` are finite sets of type `β`, and `f(a) = g(a)` for all `a` in `s₂`, then `sup (f ∘ incl s₁) = sup (g ∘ incl s₂)`, where `incl s i` denotes the inclusion map from `s i` to `β`.
|
Finset.sup_const
theorem Finset.sup_const :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β},
s.Nonempty → ∀ (c : α), (s.sup fun x => c) = c
The theorem `Finset.sup_const` states that for any types α and β, given a semilattice structure and a minimal element (order bottom) on α, and a non-empty finite set `s` of type β, the supremum of constant function `c` on this set equals to `c`. In other words, when applied to all elements of a non-empty finite set, the supremum of the constant function is just the constant itself.
More concisely: For any semilattice α with a minimal element and non-empty finite set β, the supremum of the constant function on β is equal to the constant itself.
|
Finset.min_le
theorem Finset.min_le : ∀ {α : Type u_2} [inst : LinearOrder α] {a : α} {s : Finset α}, a ∈ s → s.min ≤ ↑a
The theorem `Finset.min_le` states that for any type `α` with a linear order and for any element `a` of type `α` and finite set `s` of type `α`, if `a` is an element of `s`, then the minimum element of `s` is less than or equal to `a`. This minimum element is represented within the `WithTop α` type, which includes all elements of `α` together with a top element. Here, `↑a` is the lift of `a` to `WithTop α`.
More concisely: For any type `α` with a linear order, if `a` is an element of a finite set `s` in `α`, then the minimum element of `s` (including the top element) is less than or equal to `a` (lifted to `WithTop α`).
|
Finset.sup_induction
theorem Finset.sup_induction :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
{p : α → Prop}, p ⊥ → (∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)) → (∀ b ∈ s, p (f b)) → p (s.sup f)
The theorem `Finset.sup_induction` is a principle of mathematical induction for the supremum of a finite set in the context of semilattice and ordered bottom structure. Given a type `α` with a semilattice supremum structure and an ordered bottom structure, a finite set `s` of type `β`, a function `f` mapping `β` to `α`, and a property `p` holding over `α`, it states that if the property `p` holds for the least element `⊥` of `α`, and if `p` holds for any supremum `a₁ ⊔ a₂` whenever it holds for `a₁` and `a₂`, and finally, if `p` holds for each element of `s` under the function `f`, then `p` must also hold for the supremum of the set `s` under `f`.
More concisely: Given a semilattice and ordered bottom structure on type `α`, if a property `p(x)` holds for the least element `⊥`, the supremum `a ⊔ b` of any two elements `a` and `b` satisfying `p(a)` and `p(b)`, and each element `x ∈ s` under the function `f`, then `p(∨x in s.f : f(x))` holds, where `∨` denotes the supremum of the set `{f(x) | x ∈ s}`.
|
iInf_eq_iInf_finset'
theorem iInf_eq_iInf_finset' :
∀ {α : Type u_2} {ι' : Sort u_7} [inst : CompleteLattice α] (s : ι' → α), ⨅ i, s i = ⨅ t, ⨅ i ∈ t, s i.down := by
sorry
This theorem establishes that the greatest lower bound (infimum) of a function `s` mapping from any type `ι'` to a complete lattice `α` is equal to the greatest lower bound over all finite sets `t` of type `ι'` of the greatest lower bounds of `s i` for `i` in `t`. This version of the theorem works for `ι'` as a general sort. There is another version (`iInf_eq_iInf_finset`) that is limited to `ι'` as a type, but does not require the use of propositional lifts (`PLift`s).
More concisely: The greatest lower bound of a function from a general sort to a complete lattice equals the greatest lower bound of the function restricted to every finite subset.
|
Finset.inf'_image
theorem Finset.inf'_image :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] [inst_1 : DecidableEq β] {s : Finset γ}
{f : γ → β} (hs : (Finset.image f s).Nonempty) (g : β → α), (Finset.image f s).inf' hs g = s.inf' ⋯ (g ∘ f)
The theorem `Finset.inf'_image` is about the computation of infimum over a nonempty finset in the context of a semilattice. It states that for any types `α`, `β`, and `γ`, if we have a semilattice structure on `α` and decidable equality on `β`, and if `s` is a nonempty finset of type `γ` with a mapping `f` to `β` such that the image of `s` under `f` is nonempty, then the infimum of the image of `s` under `f` with a map `g` to `α` is the same as the infimum of `s` under the composition of `g` and `f`. In other words, it shows the compatibility of the infimum operation with the image of a function on a finset.
More concisely: For any semilattice `α`, if `s` is a nonempty finset mapped to a nonempty image under `f: γ → β`, then `inf (map f s) = inf s . map g f` for any maps `g: β → α`.
|
Finset.max_insert
theorem Finset.max_insert :
∀ {α : Type u_2} [inst : LinearOrder α] {a : α} {s : Finset α}, (insert a s).max = max (↑a) s.max
This theorem states that for any type `α` that has a linear order, any element `a` of type `α`, and any finite set `s` of type `α`, the maximum element of the set obtained by inserting `a` into `s` is equal to the maximum of `a` and the maximum element of `s`. The maximum of a set is defined to be the largest element if the set is not empty, and the bottom element otherwise.
More concisely: For any linear order type `α`, set `s` of `α`, and element `a` of `α`, the maximum of `a` and the maximum of `s` is the maximum of `s` with `a` inserted.
|
Finset.inf_singleton
theorem Finset.inf_singleton :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {f : β → α} {b : β},
{b}.inf f = f b
The theorem `Finset.inf_singleton` states that for any types `α` and `β`, given a semilattice structure and an order top structure on `α`, a function `f` from `β` to `α`, and an element `b` of type `β`, the infimum (greatest lower bound) of the singleton set `{b}` under the function `f` is equal to the function `f` applied to `b`. This means that the infimum of the image of a singleton set under a function is just the image of the single element itself.
More concisely: For any semilattice and order topology on types `α` and `β`, and any function `f` from `β` to `α` and element `b` of `β`, the infimum of the singleton set `{b}` under `f` equals `f(b)`.
|
Finset.sup_map
theorem Finset.sup_map :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset γ)
(f : γ ↪ β) (g : β → α), (Finset.map f s).sup g = s.sup (g ∘ ⇑f)
The theorem `Finset.sup_map` asserts that for any types `α`, `β`, `γ`, given a semilattice structure and smallest element (OrderBot) on `α`, for any finite set `s` of type `γ`, an injective function `f` from `γ` to `β`, and a function `g` from `β` to `α`, the supremum of the image of `s` under `f` mapped through `g` is equal to the supremum of `s` mapped through the composition of `g` and `f`. In other words, it is the property of "commutativity" of the supremum over a finite set with respect to function composition and mapping a finite set under an injective function.
More concisely: For any semilattice `α` with smallest element, injective function `f` from a finite set `s` of type `γ` to `β`, and functions `g : β -> α` and `h : α -> α` with `h = g ∘ f`, the supremum of `s` mapped through `h` is equal to the supremum of `s` mapped through `g` and then `f`.
|
Finset.inf'_le
theorem Finset.inf'_le :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} (f : β → α) {b : β} (h : b ∈ s),
s.inf' ⋯ f ≤ f b
The theorem `Finset.inf'_le` states that for any given types `α` and `β`, where `α` is a semilattice infimum, any function `f` from `β` to `α`, any element `b` of type `β` that is an element in a nonempty finite set `s` (of type `Finset β`), then the infimum of the image of the set `s` under the function `f` is less than or equal to the image of the element `b` under `f`. This essentially means that the infimum of the image of a non-empty finite set under a certain function is not greater than the function's value at any particular element in the set.
More concisely: For any semilattice infimum ℴ over types α and β, any function f from β to α, and any nonempty finite set s of β, the infimum of the image of s under f is less than or equal to the image of any element b in s under f. (i.e., ℴ(s) ≤ f(b) for all b in s).
|
Mathlib.Data.Finset.Lattice._auxLemma.31
theorem Mathlib.Data.Finset.Lattice._auxLemma.31 :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α},
(s.sup' H f ≤ a) = ∀ b ∈ s, f b ≤ a
The theorem `Mathlib.Data.Finset.Lattice._auxLemma.31` states that for any types `α` and `β`, and for any instance of a join-semilattice `α`, and for any nonempty finite set `s` of elements of type `β`, and for any function `f` from `β` to `α`, and for any element `a` of type `α`, the supremum of the image of `s` under `f` is less than or equal to `a` if and only if every element `b` in `s` has an image under `f` that is less than or equal to `a`. In mathematical terms, it's saying that $\sup(f(s)) \leq a$ if and only if for all $b \in s$, $f(b) \leq a$.
More concisely: The supremum of the image of a nonempty finite set under a function from another type is less than or equal to an element if and only if the image of every element in the set is less than or equal to that element.
|
Finset.coe_inf'
theorem Finset.coe_inf' :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α),
↑(s.inf' H f) = s.inf (WithTop.some ∘ f)
The theorem `Finset.coe_inf'` states that for any semilattice (a partially ordered set in which any two elements have a greatest lower bound) `α` and any nonempty finite set `s` of elements of type `β`, and any function `f` mapping `β` to `α`, the infimum of the image of `s` under `f` (obtained using the `Finset.inf'` function) when raised to the "with top" (a type extension that adds a new "top" element to a type) space is equal to the infimum of the image of `s` under the function composed of `f` and `WithTop.some` (which maps any element to the "with top" space). In other words, adding a top element and calculating the infimum in the resulting extended space is the same as calculating the infimum in the original space and then adding the top element.
More concisely: For any semilattice α, nonempty finite set s of elements β, and function f : β → α, the infimum of the image of s under f in the extended space with top element is equal to the infimum of the image of s under the function composed of f and the inclusion map to the extended space.
|
Finset.sup'_induction
theorem Finset.sup'_induction :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α)
{p : α → Prop}, (∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)) → (∀ b ∈ s, p (f b)) → p (s.sup' H f)
The `Finset.sup'_induction` theorem states that for all types `α` and `β`, where `α` is a join-semilattice, given a non-empty finite set `s` of type `β`, a function `f` mapping from `β` to `α`, and a property `p` that applies to elements of `α`, if `p` holds for all pairs of elements `a₁` and `a₂` such that `p` holds for both `a₁` and `a₂` separately and `p` holds for their supremum `a₁ ⊔ a₂`, and if `p` holds for all elements of the image of `s` under `f`, then `p` indeed holds for the supremum of the image of `s` under `f`. In simpler terms, the theorem provides a method of proof by induction on properties of the supremum of a function applied to elements of a finite set.
More concisely: Given a join-semilattice `α`, a non-empty finite set `s` of type `β`, a function `f` from `β` to `α`, and a property `p` that respects the join operation, if `p` holds for all elements of `s` and their images under `f`, and for all pairs of elements in `s` whose supremum exists, then `p` holds for the supremum of the images of `s` under `f`.
|
Finset.comp_sup'_eq_sup'_comp
theorem Finset.comp_sup'_eq_sup'_comp :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup γ] {s : Finset β}
(H : s.Nonempty) {f : β → α} (g : α → γ),
(∀ (x y : α), g (x ⊔ y) = g x ⊔ g y) → g (s.sup' H f) = s.sup' H (g ∘ f)
This theorem states that for any three types `α`, `β`, and `γ` where `α` and `γ` are equipped with a (possibly unbounded) join-semilattice structure, and for any nonempty finite set `s` of type `β`, a function `f` from `β` to `α`, and a function `g` from `α` to `γ`, if the function `g` preserves the join operation (i.e., `g` applied to the join of `x` and `y` equals the join of `g` applied to `x` and `g` applied to `y`), then applying `g` to the supremum of the image of `s` under `f` (denoted `Finset.sup' s H f`) is the same as first applying `g` to the elements of `s` and then taking the supremum of the resulting set (denoted `Finset.sup' s H (g ∘ f)`). In mathematical terms, it says that the supremum operation `sup'` commutes with a join-preserving function `g`.
More concisely: If `α` and `γ` are join-semilattices, `s` is a nonempty finite set of type `β`, `f : β → α`, `g : α → γ` is join-preserving, then `g (Finset.sup' s H f) = Finset.sup' s H (g ∘ f)`.
|
Finset.sup_singleton
theorem Finset.sup_singleton :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {f : β → α} {b : β},
{b}.sup f = f b
The theorem `Finset.sup_singleton` states that for any types `α` and `β`, given a semilattice structure and a least element for `α` (the type `α` endowed with a semilattice structure and a least element is known as a bounded semilattice), a function `f` from `β` to `α`, and an element `b` of `β`, the supremum of the singleton set `{b}` under the function `f` is equal to the function `f` applied to `b`. In plain language, when a set has only one element, the supremum (greatest value) of the set under a function is just the value of the function at that single element.
More concisely: For any semilattice `α` with least element, function `f` from `β` to `α`, and `b` in `β`, the supremum of the singleton set `{b}` under `f` equals `f(b)`.
|
Finset.inf_eq_iInf
theorem Finset.inf_eq_iInf :
∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] (s : Finset α) (f : α → β), s.inf f = ⨅ a ∈ s, f a := by
sorry
The theorem `Finset.inf_eq_iInf` states that for any types `α` and `β` where `β` is a complete lattice, any finite set `s` of type `α`, and any function `f` from `α` to `β`, the infimum of the set `s` under the function `f` is equal to the infimum over all elements `a` in the set `s` of `f(a)`. In other words, `Finset.inf s f` is the same as computing the infimum of `f(a)` for all `a` in `s`.
More concisely: For any complete lattice β, the infimum of a function f from a finite set s to β, over all elements in s, is equal to the infimum of the images of the elements in s under f.
|
Finset.le_max'
theorem Finset.le_max' : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (x : α) (H2 : x ∈ s), x ≤ s.max' ⋯ := by
sorry
This theorem asserts that for any type `α` that has a linear order, and any finset `s` of elements of type `α`, if an element `x` of type `α` is in the finset `s`, then `x` is less than or equal to the maximum element of `s`. This maximum is expressed as `Finset.max' s`, where `Finset.max'` function returns the maximum element of a nonempty finset in a linear order.
More concisely: For any linear order type `α` and finset `s` of elements from `α`, if `x` is an element of `s`, then `x ≤ Finset.max' s`.
|
Finset.max'_image
theorem Finset.max'_image :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
Monotone f → ∀ (s : Finset α) (h : (Finset.image f s).Nonempty), (Finset.image f s).max' h = f (s.max' ⋯)
This theorem states that for any types `α` and `β` that have a linear order, if a function `f` from `α` to `β` is monotone (meaning `f a ≤ f b` whenever `a ≤ b`), then for any finite set `s` of elements of `α`, if the image of `s` under `f` is non-empty, then the maximum element of the image of `s` under `f` is equal to the image under `f` of the maximum element of `s`. In other words, taking the maximum and then applying `f` is the same as first applying `f` and then taking the maximum, when `f` is a monotone function.
This theorem can be used to rewrite expressions from right to left when dealing with the maximum of an image of a finite set under a monotone function.
More concisely: For any monotonic function `f` between linearly ordered types `α` and `β`, and any finite subset `s` of `α` with non-empty image under `f`, the maximum value of `f` over `s` equals `f` applied to the maximum element of `s`.
|
Finset.inf'_congr
theorem Finset.inf'_congr :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} (H : s.Nonempty) {t : Finset β}
{f g : β → α} (h₁ : s = t), (∀ x ∈ s, f x = g x) → s.inf' H f = t.inf' ⋯ g
The theorem `Finset.inf'_congr` states that for any type `α` that forms a semilattice under the infimum operation, and any nonempty finite sets `s` and `t` of another type `β`, if `s` is equal to `t` and two functions `f` and `g` from `β` to `α` are equal on every element of `s`, then the infimum of the image of `s` under `f` is equal to the infimum of the image of `t` under `g`. This theorem is about the congruence of the `inf'` operation on finite sets with respect to set equality and pointwise function equality.
More concisely: For any semilattice `α`, equal finite sets `s` and `t` of type `β`, and equal functions `f` and `g` from `β` to `α`, the infimum of `f` over `s` equals the infimum of `g` over `t`.
|
Finset.exists_max_image
theorem Finset.exists_max_image :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] (s : Finset β) (f : β → α),
s.Nonempty → ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x
This theorem states that for any non-empty finite set `s` of type `β` and any function `f` from `β` to `α` (where `α` is a linearly ordered type), there exists an element `x` in `s` such that the image of `x` under `f` is greater than or equal to the image of any other element in `s` under `f`. In other words, `f(x)` is the maximum value attained by `f` on `s`.
More concisely: For any non-empty finite set `s` and function `f` from a linearly ordered type to itself, there exists an element `x` in `s` such that `f(x)` is the maximum value of `f` on `s`.
|
Finset.sup_inf_distrib_left
theorem Finset.sup_inf_distrib_left :
∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] [inst_1 : OrderBot α] (s : Finset ι) (f : ι → α) (a : α),
a ⊓ s.sup f = s.sup fun i => a ⊓ f i
The theorem `Finset.sup_inf_distrib_left` states that for any type `α` that forms a distributive lattice with a least element, a finite set `s` of elements of any type `ι`, a function `f` from `ι` to `α`, and any element `a` of `α`, the infimum (greatest lower bound) of `a` and the supremum (least upper bound) of the image of `s` under `f` is equal to the supremum of the image of `s` under the function that sends `i` to the infimum of `a` and `f(i)`. In mathematical notation, this can be expressed as `a ⊓ sup(f(s)) = sup({a ⊓ f(i) | i ∈ s})`.
More concisely: For any distributive lattice with a least element and function from a finite set to it, the infimum of an element with the supremum of its image is equal to the supremum of the infimums of the image elements.
|
map_finset_inf
theorem map_finset_inf :
∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [inst : SemilatticeInf α] [inst_1 : OrderTop α]
[inst_2 : SemilatticeInf β] [inst_3 : OrderTop β] [inst_4 : FunLike F α β] [inst_5 : InfTopHomClass F α β] (f : F)
(s : Finset ι) (g : ι → α), f (s.inf g) = s.inf (⇑f ∘ g)
The theorem `map_finset_inf` states that for all types `F`, `α`, `β`, and `ι`, with `α` and `β` being semilattice infima and ordered tops, and type `F` being a function-like object from `α` to `β` which also satisfies the `InfTopHomClass` typeclass, and given a function `f` of type `F`, a finite set `s` of type `Finset ι`, and a function `g` from `ι` to `α`, the function `f` applied to the infimum of the set `s` under function `g` equals to the infimum of the set `s` under the composition of `f` and `g`. In simpler terms, this theorem is about the commutativity of the function `f` with the operation of taking the infimum over a finite set.
More concisely: For any semilattice infima and ordered tops types `α` and `β`, function-like object `F` from `α` to `β` belonging to `InfTopHomClass`, and finite set `s` of index type `ι`, the function `f : F` applied to the infimum of `s` under `g : ι → α` is equal to the infimum of `s` under the composition `f ∘ g`.
|
Finset.min'_eq_inf'
theorem Finset.min'_eq_inf' :
∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty), s.min' H = s.inf' H id
The theorem `Finset.min'_eq_inf'` states that for any given non-empty finset `s` of a type `α` that has a linear order, the minimum element of `s` (`Finset.min' s H`) is equal to the infimum (`Finset.inf' s H id`) of `s` when considering the identity function. Here, `H` is a proof that set `s` is nonempty. This theorem bridges the concepts of minimum of a set and the infimum of a set under the identity map in the context of a finite set in Lean 4.
More concisely: For any non-empty finite set `s` with a linear order, `Finset.min' s` equals `Finset.inf' s` under the identity function.
|
Finset.sup_product_left
theorem Finset.sup_product_left :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Finset β)
(t : Finset γ) (f : β × γ → α), (s ×ˢ t).sup f = s.sup fun i => t.sup fun i' => f (i, i')
The theorem `Finset.sup_product_left` states that for any types `α`, `β`, and `γ`, with `α` being orderable with a least element and also being a semilattice with respect to the supremum operation, and given two finite sets `s` of type `β` and `t` of type `γ`, along with a function `f` that maps pairs of elements from `β` and `γ` to `α`, the supremum of the function `f` over the Cartesian product of `s` and `t` is equal to the supremum of the function `f` over each element `i` of `s` and each element `i'` of `t`. In other words, it states that the supremum operation distributes over the Cartesian product of two finite sets.
More concisely: For any orderable semilattice α with least element, and finite sets s:β and t:γ, the function sup (λ (i, j): s × t → α) = sup (i: s → α) ⊤ (sup (j: t → α) j) where ⊤ is the constant function mapping all elements to the least element of α.
|
Finset.inf'_comp_eq_image
theorem Finset.inf'_comp_eq_image :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] [inst_1 : DecidableEq β] {s : Finset γ}
{f : γ → β} (hs : s.Nonempty) (g : β → α), s.inf' hs (g ∘ f) = (Finset.image f s).inf' ⋯ g
The theorem `Finset.inf'_comp_eq_image` states that for any given types `α`, `β`, and `γ`, where `α` has a semilattice structure and `β` has decidable equality, and for any given nonempty finite set of elements from `γ` (denoted by `s`), and functions `f : γ → β` and `g : β → α`, the infimum (greatest lower bound) of the set obtained by applying the function composition `g ∘ f` on the elements of `s` is the same as the infimum of the set obtained by applying the function `g` on the image of `s` under the function `f`. This theorem essentially bridges the concept of function composition and the operation of taking the infimum in the context of finite sets.
More concisely: For any semilattice `α` with decidable equality, function `f : γ → β`, nonempty finite set `s ⊆ γ`, and function `g : β → α`, the infimum of `g ∘ f` applied to `s` equals the infimum of `g` applied to the image of `s` under `f`.
|
Finset.isGreatest_max'
theorem Finset.isGreatest_max' :
∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty), IsGreatest (↑s) (s.max' H)
The theorem `Finset.isGreatest_max'` states that for any nonempty finite set `s` in a linear order `α`, the maximum element of `s`, denoted by `Finset.max' s H`, is the greatest element of `s`. Here, `H` is a proof of non-emptiness of the set `s`. The function `IsGreatest` ensures that this maximum element is actually part of the set `s` and that no element in `s` is greater than it. Therefore, this theorem verifies the correctness of the `Finset.max'` function in the context of linearly ordered finite sets.
More concisely: For any nonempty finite subset `s` of a linearly ordered set `α`, the maximum element ` Finset.max' s H` is the greatest element of `s`.
|
Finset.sup'_product_left
theorem Finset.sup'_product_left :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] {s : Finset β} {t : Finset γ}
(h : (s ×ˢ t).Nonempty) (f : β × γ → α), (s ×ˢ t).sup' h f = s.sup' ⋯ fun i => t.sup' ⋯ fun i' => f (i, i')
The theorem `Finset.sup'_product_left` states that for any finite nonempty sets `s` of type `β` and `t` of type `γ`, any type `α` that is a join-semilattice, and any function `f` from the product of `β` and `γ` to `α`, the supremum of the image of the product set `s ×ˢ t` under `f` is equal to the supremum of the image of `s` under the function that maps each element of `s` to the supremum of the image of `t` under the function that maps each element of `t` to `f` applied to the pair of elements from `s` and `t`. Essentially, this theorem shows that the operation of taking supremums over a product set can be decomposed into taking supremums over each of the sets separately.
More concisely: For any join-semilattice α, finite nonempty sets s:β and t:γ, and function f:β × γ → α, the supremum of f(s ×ˢ t) equals the supremum of the image of s under the function mapping each s i to the supremum of f(t) applied to each t j.
|
Finset.sup'_congr
theorem Finset.sup'_congr :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (H : s.Nonempty) {t : Finset β}
{f g : β → α} (h₁ : s = t), (∀ x ∈ s, f x = g x) → s.sup' H f = t.sup' ⋯ g
This theorem states that for any type `α` that forms a join-semilattice, and any nonempty finite sets `s` and `t` of type `β`, along with two functions `f` and `g` mapping from `β` to `α`, if `s` and `t` are identical sets (i.e., `s = t`), and for every element `x` in `s`, `f(x)` equals `g(x)`, then the supremum of the image of `s` under `f` is equal to the supremum of the image of `t` under `g`. In other words, if two nonempty finite sets are the same and two functions agree on every element of these sets, then the supremum of the sets under these functions will also be the same.
More concisely: If `α` is a join-semilattice, `s` and `t` are identical nonempty finite sets, and `f(x) = g(x)` for all `x` in `s`, then `sup (map f s) = sup (map g t)`.
|
Finset.prodMk_inf'_inf'
theorem Finset.prodMk_inf'_inf' :
∀ {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β]
{s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β),
(s.inf' hs f, t.inf' ht g) = (s ×ˢ t).inf' ⋯ (Prod.map f g)
The theorem `Finset.prodMk_inf'_inf'` states that for any types `ι`, `κ`, `α`, and `β`, where `α` and `β` are semilattice inf structures, given two nonempty finite sets `s` of type `ι` and `t` of type `κ`, along with functions `f : ι → α` and `g : κ → β`, the pair formed by the infimum of `s` mapped by `f` and the infimum of `t` mapped by `g` is equal to the infimum of the Cartesian product of `s` and `t`, where each pair in the product is mapped by the function `Prod.map f g`. In other words, the infimum of the mapped values in the individual sets, when made into a pair, is the same as the infimum of the mapped pairs in the combined set.
More concisely: For any semilattices α and β, and nonempty finite sets s : ι, t : κ, the infimum of the maps f : ι → α and g : κ → β of s and t, respectively, equals the infimum of the pairs (s i, t j) mapped by Prod.map f g.
|
Finset.le_max_of_eq
theorem Finset.le_max_of_eq :
∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α} {a b : α}, a ∈ s → s.max = ↑b → a ≤ b
The theorem `Finset.le_max_of_eq` states that for any given type `α` that has a linear order, and for any finite set `s` of elements of this type, if an element `a` belongs to `s` and the maximum value of `s` is `b`, then `a` is less than or equal to `b`. This ensures that any element of a finite set is always less than or equal to the maximum of that set.
More concisely: For any type `α` with a linear order and any finite set `s` of elements from `α`, if `a` is an element of `s` and `b` is the maximum element of `s`, then `a ≤ b`.
|
Finset.max'_singleton
theorem Finset.max'_singleton : ∀ {α : Type u_2} [inst : LinearOrder α] (a : α), {a}.max' ⋯ = a
This theorem states that for any given type `α`, which has a linear ordering, the maximum element of a singleton set containing only element `a` (expressed as `{a}.max' _`) is `a` itself. In other words, the maximum value of a set with only one element is the element itself.
More concisely: For any linear ordered type `α` and element `a` in `α`, the maximum element of the singleton set `{a}` is `a` itself.
|
Finset.sup_insert
theorem Finset.sup_insert :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
[inst_2 : DecidableEq β] {b : β}, (insert b s).sup f = f b ⊔ s.sup f
The theorem `Finset.sup_insert` states that for any types `α` and `β`, given a semilattice structure (where supremum operation is possible) on `α` and the bottom element of `α`, a finite set `s` of type `β`, and a function `f` mapping from `β` to `α`. If type `β` has decidable equality, and `b` is an element of type `β`, then the supremum of the set formed by inserting `b` into `s` mapped through `f` is equal to the supremum of `f(b)` and the supremum of the set `s` mapped through `f`. In simpler terms, adding an element to a finite set and then taking the supremum, is the same as taking the supremum of the original set and the new element separately.
More concisely: Given a semilattice with bottom element, a finite set, and a function from the set to the semilattice with decidable equality, the supremum of the set with a new element inserted and mapped through the function equals the supremum of mapping the new element through the function and the original supremum.
|
Finset.inf'_cons
theorem Finset.inf'_cons :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) {b : β}
{hb : b ∉ s}, (Finset.cons b s hb).inf' ⋯ f = f b ⊓ s.inf' H f
This theorem states that for any types `α` and `β`, with `α` being a semilattice, any nonempty finite set `s` of `β`, function `f` mapping `β` to `α`, and any element `b` of `β` not in `s`, the infimum of the image under `f` of the set obtained by adding `b` to `s` is equal to the infimum of `f(b)` and the infimum of the image under `f` of `s`. In other words, it describes how the infimum of a set changes when a new element is added to it.
More concisely: For any semilattice `α`, function `f` from `β` to `α`, nonempty finite set `s` of `β`, and `b` not in `s`, the infimum of `{f(x) | x ∈ s ∪ {b}}` equals the infimum of `{f(x) | x ∈ s}` and `f(b)`.
|
Finset.sup'_apply
theorem Finset.sup'_apply :
∀ {α : Type u_2} {β : Type u_3} {C : β → Type u_7} [inst : (b : β) → SemilatticeSup (C b)] {s : Finset α}
(H : s.Nonempty) (f : α → (b : β) → C b) (b : β), s.sup' H f b = s.sup' H fun a => f a b
The theorem `Finset.sup'_apply` states that for any types `α`, `β`, `C`, and a function `f` from `α` to `C b` for each `b` in `β`, along with a non-empty finset `s` of `α`, and any `b` in `β`, the supremum of the image of `s` under `f` evaluated at `b` is equal to the supremum of the image of `s` under the function that maps each element `a` of `s` to `f a b`. This holds in a possibly unbounded join-semilattice `C b` for each `b` in `β`.
More concisely: For any type `α`, types `β` and `C`, function `f` from `α` to `C(β)`, non-empty finset `s` of `α`, and `b` in `β`, the supremum of `f` applied element-wise to `s` equals the supremum of `f` applied to each element of `s` and then evaluated at `b`.
|
Finset.min'_image
theorem Finset.min'_image :
∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
Monotone f → ∀ (s : Finset α) (h : (Finset.image f s).Nonempty), (Finset.image f s).min' h = f (s.min' ⋯)
This theorem states that for any types `α` and `β` with a linear order, given a function `f` from `α` to `β` that is monotone (i.e., `f` preserves order), and a nonempty finite set `s` of type `α`, the smallest element of the forward image of `s` under `f` (i.e., `Finset.image f s`) is the same as the image under `f` of the smallest element of `s`. In other words, applying `f` to the smallest element of `s` gives the smallest element in the image of `s` under `f`, assuming `f` is a monotone function.
More concisely: For any monotone function `f` between linearly ordered types `α` and `β`, and any nonempty finite subset `s` of `α`, the smallest element of `f''s` is `f` applied to the smallest element of `s`.
|
Finset.sup_id_eq_sSup
theorem Finset.sup_id_eq_sSup : ∀ {α : Type u_2} [inst : CompleteLattice α] (s : Finset α), s.sup id = sSup ↑s := by
sorry
The theorem `Finset.sup_id_eq_sSup` states that for all types `α` that are complete lattices, and for any finite set `s` of type `α`, the supremum of `s` when computed via the function `Finset.sup` with the identity function is the same as the supremum (`sSup`) of the set obtained by coercing `s` into a set. In other words, it says that calculating the supremum of `s` by taking the supremum of the identity function at each of its elements is equivalent to directly calculating the supremum of `s` in the complete lattice `α`.
More concisely: For any complete lattice α and finite set s of type α, the supremum of s computed using the identity function is equal to the direct supremum of s.
|
Finset.sup'_image
theorem Finset.sup'_image :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : DecidableEq β] {s : Finset γ}
{f : γ → β} (hs : (Finset.image f s).Nonempty) (g : β → α), (Finset.image f s).sup' hs g = s.sup' ⋯ (g ∘ f)
The theorem `Finset.sup'_image` states that for any types `α`, `β`, and `γ`, where `α` is a semilattice with a supremum operation, `β` has a decidable equality, and `s` is a non-empty `Finset` of type `γ`, for any function `f` mapping `γ` to `β` and `g` mapping `β` to `α`, the supremum of the image of `s` under `f`, followed by `g`, is the same as the supremum of `s` under the composition of `g` and `f`. This essentially says that the order of applying `f` and `g` does not matter when computing the supremum of the transformed `Finset`.
More concisely: For any semilattice `α` with decidable equality, non-empty `Finset` `s` of type `γ`, and functions `f: γ → β` and `g: β → α`, the supremum of `s` under `g ∘ f` equals the supremum of `s` under `g` then `f`.
|
Finset.inf'_eq_inf
theorem Finset.inf'_eq_inf :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} (H : s.Nonempty)
(f : β → α), s.inf' H f = s.inf f
The theorem `Finset.inf'_eq_inf` states that for any semilattice (a partially ordered set with a greatest lower bound for any pair of elements) of type α, with the presence of a top element, and any finite set `s` of type β that is nonempty, the infimum of the image of `s` under a function `f` obtained using `Finset.inf'` method is equal to the infimum obtained using `Finset.inf` method. In other words, both `Finset.inf' s H f` and `Finset.inf s f` will yield the same result when `s` is nonempty. The function `f` maps elements from the set `s` to the semilattice α.
More concisely: For any semilattice with a top element and nonempty finite set, the infimum of the image of the set under a function, as computed using `Finset.inf'` and `Finset.inf`, is equal.
|
Finset.mem_of_min
theorem Finset.mem_of_min : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α} {a : α}, s.min = ↑a → a ∈ s := by
sorry
This theorem, named `Finset.mem_of_min`, says that for any given set `s` of a type `α` that has a linear order, and any element `a` of type `α`, if the minimum value of the set `s` is equal to `a` (denoted in Lean 4 by `Finset.min s = ↑a`), then `a` must be an element of the set `s`. In plain English, if a number is the minimum of a set, it is necessarily a member of that set. This theorem holds for any type `α` that has a defined linear order.
More concisely: If `s` is a linearly ordered set and `a` is its minimum element, then `a` belongs to `s`.
|
Finset.sup_le_iff
theorem Finset.sup_le_iff :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α} {a : α},
s.sup f ≤ a ↔ ∀ b ∈ s, f b ≤ a
The theorem `Finset.sup_le_iff` states that for any types `α` and `β`, where `α` is a semilattice sup and has a bottom element, and given a finite set `s` of type `β`, a function `f` from `β` to `α`, and an element `a` of type `α`, the supremum of the set `s` under function `f` is less than or equal to `a` if and only if every element `b` in `s` satisfies `f(b)` is less than or equal to `a`. In mathematical terms, this can be written as: $\sup_{b\in s}f(b)\leq a \iff \forall b\in s, f(b)\leq a$.
More concisely: For any semilattice sup type `α` with a bottom element, function `f` from a finite set `s` of type `β` to `α`, and element `a` of type `α`, the supremum of `f(s)` is less than or equal to `a` if and only if every `b` in `s` satisfies `f(b)` is less than or equal to `a`.
|
Finset.inf'_comp_eq_map
theorem Finset.inf'_comp_eq_map :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] {s : Finset γ} {f : γ ↪ β} (g : β → α)
(hs : s.Nonempty), s.inf' hs (g ∘ ⇑f) = (Finset.map f s).inf' ⋯ g
The theorem `Finset.inf'_comp_eq_map` states that for any types `α`, `β`, and `γ`, given `α` is a semilattice, a nonempty finset `s` of type `γ`, and an embedding `f` from `γ` to `β`, the infimum of the composition of a function `g` (from `β` to `α`) and `f` over the finset `s` is equal to the infimum of the function `g` over the image of `s` under the embedding `f`. This theorem reverses the left-hand side (LHS) and right-hand side (RHS) of the previous theorem `Finset.inf'_map` and requires that `s` is nonempty instead of its image.
More concisely: For any semilattices `α`, `β`, nonempty finset `s` of type `γ`, and embeddings `f: γ → β` and `g: β → α`, the infimum of `g ∘ f` over `s` equals the infimum of `g` over `f''(s)`.
|
Finset.le_inf
theorem Finset.le_inf :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {f : β → α} {a : α},
(∀ b ∈ s, a ≤ f b) → a ≤ s.inf f
This theorem, `Finset.le_inf`, states that for any types `α` and `β`, with `α` being a semilattice with an associated "top" element, a given set `s` of type `Finset β`, a function `f` mapping from `β` to `α`, and an element `a` of type `α`: if `a` is less than or equal to the function `f` evaluated at each element `b` in the set `s`, then `a` is also less than or equal to the infimum of the set `s` under the function `f`. The infimum here is defined as the greatest lower bound of the function applied to the elements of the set.
More concisely: For any semilattice `α` with top element, function `f` from type `β` to `α`, set `s` of type `Finset β`, and element `a` of type `α`, if `a ≤ f(b)` for all `b` in `s`, then `a ≤ ∧ x in s. f(x)`, where `∧` denotes the infimum under the function `f`.
|
Finset.inf_image
theorem Finset.inf_image :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] [inst_1 : OrderTop α]
[inst_2 : DecidableEq β] (s : Finset γ) (f : γ → β) (g : β → α), (Finset.image f s).inf g = s.inf (g ∘ f)
This theorem states that for any set `s` of type `γ`, functions `f : γ → β` and `g : β → α`, and under the conditions that `α` has a semilattice structure and a top element, and `β` has decidable equality, the infimum of the image of `s` under `f` with respect to `g` is equal to the infimum of `s` with respect to the composition of `g` and `f`. In mathematical terms, if we denote the infimum of a set `X` with respect to a function `h` by `inf(X, h)`, the theorem can be written as `inf(f(S), g) = inf(S, g ∘ f)`, where `S` is a finite set, `f` is a function mapping elements of `S` to another set, and `g` is a function mapping the image of `S` under `f` to a semilattice.
More concisely: For any finite set `S` and functions `f : S → β` and `g : β → α` where `α` is a semilattice with top element and `β` has decidable equality, `inf(f(S), g) = inf(S, g ∘ f)`.
|
Finset.min'_le
theorem Finset.min'_le : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (x : α) (H2 : x ∈ s), s.min' ⋯ ≤ x := by
sorry
The theorem `Finset.min'_le` states that for any type `α` that has a linear order structure, for any finite set `s` of elements of `α`, and for any element `x` of `α` that belongs to `s`, the minimum element of `s` (obtained by the function `Finset.min'`) is less than or equal to `x`. This means, in the context of an ordered set, the minimum element is either equal to or smaller than all other elements in the set.
More concisely: For any type `α` with a linear order structure, and for any finite set `s ⊆ α` and `x ∈ s`, the minimum element `m` of `s` satisfies `m ≤ x`.
|
Finset.le_inf'
theorem Finset.le_inf' :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α},
(∀ b ∈ s, a ≤ f b) → a ≤ s.inf' H f
The theorem `Finset.le_inf'` states that for any types `α` and `β` with `α` being a meet-semilattice, for any nonempty finite set `s` of type `β`, any function `f` from `β` to `α`, and any element `a` of type `α`, if `a` is less than or equal to the image of every element of `s` under `f`, then `a` is less than or equal to the infimum of the image of `s` under `f`. This infimum of the image under `f` is computed using the function `Finset.inf'`.
More concisely: For any meet-semilattice `α`, if `f : β → α` is a function and `a ∈ α` satisfies `a ≤ f x` for all `x ∈ nonempty finite s : β`, then `a ≤ Finset.inf' s f`.
|
Finset.sup_union
theorem Finset.sup_union :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s₁ s₂ : Finset β} {f : β → α}
[inst_2 : DecidableEq β], (s₁ ∪ s₂).sup f = s₁.sup f ⊔ s₂.sup f
This theorem, named `Finset.sup_union`, states that for any type `α` under a semilattice with a least element and any type `β` with decidable equality, given two finite sets `s₁` and `s₂` of type `β` and a function `f` from `β` to `α`, the supremum of the union set `s₁ ∪ s₂` under the function `f` is equal to the supremum of the set `s₁` under `f` joined with the supremum of the set `s₂` under `f`. In mathematical terms, for all `s₁, s₂` subsets of `β`, and for all `f : β → α`, we have `sup (s₁ ∪ s₂) f = sup s₁ f ⊔ sup s₂ f`.
More concisely: For any semilattice with a least element and decidable equality type `β`, and given finite sets `s₁` and `s₂` and a function `f` from `β` to a semilattice with identity `α`, the supremum of `f` applied to the union of `s₁` and `s₂` equals the join of the supremum of `f` on `s₁` and the supremum of `f` on `s₂`.
|
Finset.sup'_inf_distrib_left
theorem Finset.sup'_inf_distrib_left :
∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α),
a ⊓ s.sup' hs f = s.sup' hs fun i => a ⊓ f i
The theorem `Finset.sup'_inf_distrib_left` states that for any non-empty finite set `s` of type `ι`, a distributive lattice `α`, a function `f : ι → α`, and an element `a` of `α`, the infimum of `a` and the supremum of the image of `s` under `f` is equal to the supremum of the image of `s` under the function `(i => a ⊓ f i)`. In other words, this theorem guarantees the left distributivity of the infimum operation over the supremum operation for any non-empty finite set in a distributive lattice.
More concisely: For any non-empty finite set `s`, distributive lattice `α`, function `f : ι → α`, and element `a` in `α`, `inf a ⊤ (map f s) = ⊤ (map (λ i, a ⊓ f i) s)`.
|
Finset.induction_on_min
theorem Finset.induction_on_min :
∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : DecidableEq α] {p : Finset α → Prop} (s : Finset α),
p ∅ → (∀ (a : α) (s : Finset α), (∀ x ∈ s, a < x) → p s → p (insert a s)) → p s
This theorem states an induction principle for finite sets (`Finset`s) in a linearly ordered type. The principle asserts that a property, denoted by `p`, holds for all finite sets of a certain type, given two conditions:
1. The property holds for the empty set.
2. For any finite set `s` and an element `a` which is strictly less than all elements in `s`, if the property holds for `s`, then it also holds when `a` is inserted into `s`.
The theorem formalizes the idea of proving a statement about finite sets by gradually increasing the set, one element at a time, from the smallest possible set (the empty set).
More concisely: The theorem asserts that a property holds for all finite subsets of a linearly ordered type if it holds for the empty set and is preserved under adding an element strictly less than all elements in the set.
|
Finset.inf'_map
theorem Finset.inf'_map :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] {s : Finset γ} {f : γ ↪ β} (g : β → α)
(hs : (Finset.map f s).Nonempty), (Finset.map f s).inf' hs g = s.inf' ⋯ (g ∘ ⇑f)
The theorem `Finset.inf'_map` states that for any types `α`, `β`, and `γ`, with `α` being a semilattice-inf, any finset `s` of type `γ`, an embedding function `f` from `γ` to `β`, and a function `g` from `β` to `α`, and given that the image of `s` under `f` is nonempty, the infimum of the image of `s` under `f` with respect to `g` is equal to the infimum of `s` with respect to the composition of `g` and `f`. In other words, it's showing that mapping a function over a set and then taking the infimum is the same as taking the infimum of the original set with respect to the composition of the two functions.
More concisely: For any semilattice-inf type `α`, any finset `s` of type `γ`, an embedding function `f` from `γ` to `β`, and a function `g` from `β` to `α`, if `f``(s)` is nonempty, then `∧(g ∘ f)(s) = ∧(g)(∧(f)(s))`.
|
Finset.sup_mono
theorem Finset.sup_mono :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s₁ s₂ : Finset β} {f : β → α},
s₁ ⊆ s₂ → s₁.sup f ≤ s₂.sup f
The theorem `Finset.sup_mono` states that for any two finite sets `s₁` and `s₂` of type `β` and any function `f` from `β` to a type `α` equipped with a semilattice and a bottom element, if `s₁` is a subset of `s₂`, then the supremum of the image of `s₁` under `f` is less than or equal to the supremum of the image of `s₂` under `f`. In other words, if you take two sets where one is a subset of the other and apply a function to each element of these sets, the "largest" result you get from the smaller set will not be larger than the "largest" result you get from the larger set.
More concisely: For any finite sets $s\_1 \subseteq s\_2$ of type $\beta$, and any function $f : \beta \to (\alpha, \sqcup, \bot)$ with $\alpha$ being a semilattice and $\bot$ its bottom element, we have $\sup \left( f[s\_1] \right) \leq \sup \left( f[s\_2] \right)$.
|
Finset.sup'_prodMap
theorem Finset.sup'_prodMap :
∀ {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β]
{s : Finset ι} {t : Finset κ} (hst : (s ×ˢ t).Nonempty) (f : ι → α) (g : κ → β),
(s ×ˢ t).sup' hst (Prod.map f g) = (s.sup' ⋯ f, t.sup' ⋯ g)
The theorem `Finset.sup'_prodMap` states that for any types `ι`, `κ`, `α`, and `β`, with `α` and `β` both being semilattice sups, given nonempty finsets `s` of type `ι` and `t` of type `κ`, and functions `f` and `g` from `ι` to `α` and `κ` to `β` respectively, the supremum of the Cartesian product of `s` and `t` after applying the function `Prod.map f g` is equal to the pair consisting of the suprema of `s` with function `f` and `t` with function `g`. In mathematical terms, it says that $\sup_{s\times t}(f\times g) = (\sup_s f, \sup_t g)$.
More concisely: For any semilattice suprema α and β over types ι and κ, respectively, and nonempty finsets s of type ι and t of type κ, the supremum of their Cartesian product applied with functions f : ι -> α and g : κ -> β is equal to the pair (sup\_s f, sup\_t g) of their respective suprema.
|
Finset.mem_sup
theorem Finset.mem_sup :
∀ {α : Type u_7} {β : Type u_8} [inst : DecidableEq β] {s : Finset α} {f : α → Finset β} {x : β},
x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v
This theorem states that for any type `α` and `β` with `β` having decidable equality, given a finite set `s` of type `α`, a function `f` mapping each element of `s` to a finite set of type `β`, and an element `x` of type `β`, the element `x` belongs to the supremum of `s` under the function `f` if and only if there exists an element `v` in `s` such that `x` belongs to the finite set that `f` maps `v` to. In other words, `x` is in the supremum of the image of `s` under `f` precisely when `x` is in the image of some element of `s` under `f`.
More concisely: For any finite set `s` of type `α` and function `f` from `s` to the finite sets of type `β`, an element `x` of type `β` belongs to the supremum of the image of `s` under `f` if and only if there exists `v` in `s` such that `x` is in the image of `v` under `f`.
|
Finset.max_eq_sup_coe
theorem Finset.max_eq_sup_coe : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α}, s.max = s.sup WithBot.some := by
sorry
This theorem states that for any given type `α` which has a linear order and any finite set `s` of `α`, the maximum value of `s` is equal to the supremum of `s` when each element of `s` is mapped into `WithBot α` using the canonical map. In other words, the max function on a finite set equals to applying the supremum function to the same set after each of its elements has been lifted into the `WithBot α` type.
More concisely: For any finite set `s` of a linearly ordered type `α`, the maximum element of `s` is equal to the supremum of the images of `s` under the canonical map to `WithBot α`.
|
Finset.min'_lt_max'_of_card
theorem Finset.min'_lt_max'_of_card :
∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (h₂ : 1 < s.card), s.min' ⋯ < s.max' ⋯
The theorem `Finset.min'_lt_max'_of_card` states that for any finite set `s` of a linearly ordered type `α`, if the set `s` contains more than one element, then the minimum element of `s` is strictly less than the maximum element of `s`. This theorem is an alternative version of the theorem `min'_lt_max'`, and is sometimes more convenient to use in certain contexts.
More concisely: For any finite linearly ordered set `s` with more than one element, the minimum element is strictly less than the maximum element.
|
Finset.max_eq_sup_withBot
theorem Finset.max_eq_sup_withBot :
∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α), s.max = s.sup WithBot.some
This theorem states that for any finite set `s` of type `α`, where `α` is a type equipped with a linear order, the maximum of `s` is equal to the supremum of `s` with a function `WithBot.some` applied to each element. This `WithBot.some` function simply converts an element from `α` to `WithBot α`. In other words, the maximum element of a finite set in a linear order is the same as the supremum of the set when each element is lifted into an extended type that includes a "bottom" element.
More concisely: For any finite set `s` in a linearly ordered type `α`, the maximum element is equal to the supremum of `s` when each element is lifted to `WithBot α`.
|
Finset.set_biUnion_insert
theorem Finset.set_biUnion_insert :
∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] (a : α) (s : Finset α) (t : α → Set β),
⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x
This theorem states that for any type `α` and `β` with `α` having decidable equality, given an element `a` of type `α`, a finite set `s` of `α`, and a function `t` mapping elements of `α` to sets of `β`, the union over all elements in the set obtained by inserting `a` into `s` under the function `t` is equivalent to the union of the set under the function `t` at `a` and the union over all elements in `s` under the function `t`. In other words, the process of union over a set doesn't change if we extract one element and perform the union separately.
More concisely: For any type `α` with decidable equality, given an element `a` of type `α`, a finite set `s` of `α`, and a function `t` mapping elements of `α` to sets of `β`, the set `(s.insert a).map t |>.union <| t a |>.union s.map t` equals `t a |>.union (s.map t)`.
|
Finset.le_sup'
theorem Finset.le_sup' :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (f : β → α) {b : β} (h : b ∈ s),
f b ≤ s.sup' ⋯ f
The theorem `Finset.le_sup'` states that for any types `α` and `β`, where `α` has a semilattice superstructure, for any function `f` mapping from `β` to `α`, and for any element `b` of a nonempty finite set `s` of type `β`, the image of `b` under `f` is less than or equal to the supremum of the images of the elements of `s` under `f`. In other words, for all `b` in the set `s`, `f(b)` is less than or equal to the supremum of `f(s)`.
More concisely: For any semilattice `α`, function `f` from a nonempty finite set `β` to `α`, and element `b` in `β`, we have `f(b) ≤ sup(map f s)`, where `s` is the set and `map f s` is the image of `s` under `f`.
|
Set.iUnion_eq_iUnion_finset'
theorem Set.iUnion_eq_iUnion_finset' :
∀ {α : Type u_2} {ι' : Sort u_7} (s : ι' → Set α), ⋃ i, s i = ⋃ t, ⋃ i ∈ t, s i.down
The theorem `Set.iUnion_eq_iUnion_finset'` states that for any type `α` and an indexed family of sets `s : ι → Set α`, the union of this indexed family of sets is equal to the union of the unions of finite subfamilies of this indexed family. This version works for any sort `ι`. There is also a version called `iUnion_eq_iUnion_finset` that assumes `ι : Type*` but avoids `PLift`s in the right hand side. In symbols, this is saying that $\bigcup_{i \in I} s_i = \bigcup_{t \in T} \bigcup_{i \in t} s_{i.down}$, where `s_i` is the `i`-th set of the indexed family `s`, and `t` is a finite subset of the index set.
More concisely: For any type `α` and indexed family `s : ι → Set α`, the union of `s` equals the union of unions of finite subfamilies of `s`. In mathematical notation, this is $\bigcup\_{i \in I} s\_i = \bigcup\_{t \subseteq I} \bigcup\_{i \in t} s\_i$.
|