LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Order.CompleteLattice

`iInf_true` theorem iInf_true : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : True → α}, iInf s = s trivial The theorem `iInf_true` states that for any type `α` that forms a complete lattice, and for any function `s` from the type `True` (containing a single element) to `α`, the indexed infimum (`iInf`) of `s` is equal to `s` applied to `trivial`. Here, `trivial` is a term of type `True`, essentially the single value that the `True` type contains. Essentially, it says that if we take the least element over all elements returned by `s` for every possible input (in this case there's only one, `trivial`), we just get `s trivial`. More concisely: For any complete lattice `α` and function `s : True → α`, the indexed infimum `iInf (s : α)` equals `s trivial`.
`iInf_subtype` theorem iInf_subtype : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {p : ι → Prop} {f : Subtype p → α}, iInf f = ⨅ i, ⨅ (h : p i), f ⟨i, h⟩ This theorem states that for all types `α` and `ι`, where `α` is a complete lattice, and for all properties `p` over `ι` and a function `f` from the subtype of `ι` satisfying `p` to `α`, the indexed infimum of `f` is equal to the infimum over all `i` in `ι` and for all proofs `h` that `i` satisfies `p`, of `f` applied to the subtype element `{ val := i, property := h }`. In simpler terms, it says that we can compute the infimum of a function applied to elements of a subtype either directly or by considering the elements of the original type that satisfy the defining property of the subtype. More concisely: For any complete lattice `α` and property `p` over type `ι`, if `f` is a function from the subtype of `ι` satisfying `p` to `α`, then the infimum of `f` over the subtype equals the infimum of `f(i)` over all `i` in `ι` and all proofs `h` that `i` satisfies `p`.
`iSup_univ` theorem iSup_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α}, ⨆ x ∈ Set.univ, f x = ⨆ x, f x This theorem, `iSup_univ`, states that for any types `α` and `β`, where `α` is a complete lattice, and for any function `f` from `β` to `α`, the supremum (⨆) of the function `f` over all elements `x` in the universal set of `β` is the same as the supremum of the function `f` over all elements `x` of type `β`. In other words, taking the supremum of the function `f` over the universal set (which contains all elements of `β`) is equivalent to taking the supremum of `f` over the entire type `β`. More concisely: For any complete lattice α and function f from type β to α, the supremum of f over the universal set of β equals the supremum of f over type β.
`CompleteLattice.le_sInf` theorem CompleteLattice.le_sInf : ∀ {α : Type u_9} [self : CompleteLattice α] (s : Set α) (a : α), (∀ b ∈ s, a ≤ b) → a ≤ sInf s This theorem states that for any type `α` that forms a complete lattice, given any set `s` of elements of type `α` and any element `a` from `α`, if `a` is a lower bound for set `s` (meaning `a` is less than or equal to every element `b` in `s`), then `a` is also less than or equal to the infimum (greatest lower bound) of set `s`. More concisely: For any complete lattice `α` and set `s ⊆ α`, if `a` is a lower bound of `s`, then `a ≤ ⨄ s` where `⨄ s` denotes the infimum (greatest lower bound) of `s`.
`CompleteLattice.le_top` theorem CompleteLattice.le_top : ∀ {α : Type u_9} [self : CompleteLattice α] (x : α), x ≤ ⊤ This theorem states that for any type `α` that is a complete lattice, any element `x` of type `α` is less than or equal to the top element (denoted by `⊤`). In the context of lattice theory, the top element is the greatest element in the set, so this theorem is essentially saying that any element in a complete lattice is less than or equal to the greatest element in that lattice. More concisely: In a complete lattice, every element is less than or equal to the lattice's top element.
`Monotone.iSup_nat_add` theorem Monotone.iSup_nat_add : ∀ {α : Type u_1} [inst : CompleteLattice α] {f : ℕ → α}, Monotone f → ∀ (k : ℕ), ⨆ n, f (n + k) = ⨆ n, f n := by sorry This theorem states that for any type `α` that forms a complete lattice, and any function `f` mapping natural numbers to elements of `α`, if `f` is a monotone function, then for any natural number `k`, the supremum of the set `{f(n + k) \| n ∈ ℕ}` is the same as the supremum of the set `{f(n) \| n ∈ ℕ}`. In other words, if you have a monotone function from the natural numbers to a complete lattice, then adding a constant to the input of the function doesn't change the supremum of the function's values. More concisely: Let `α` be a complete lattice and `f : ℕ → α` be a monotone function; then for all natural numbers `k`, the supremum of `{f(n + k) \| n ∈ ℕ}` equals the supremum of `{f(n) \| n ∈ ℕ}`.
`le_sInf_iff` theorem le_sInf_iff : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α}, a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b The theorem `le_sInf_iff` states that for any type `α` which is a complete semilattice with respect to the infimum operation, any set `s` of elements of type `α`, and any element `a` of type `α`, the condition `a` being less than or equal to the infimum of `s` is equivalent to the condition that `a` is less than or equal to every element in `s`. In other words, an element is less than or equal to the greatest lower bound of a set if and only if it is less than or equal to every element in the set. More concisely: For any complete semilattice `α` and set `s ∈ α`, an element `a ∈ α` satisfies `a ≤ inf s` if and only if `a ≤ x` for all `x ∈ s`.
`iInf_mono'` theorem iInf_mono' : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [inst : CompleteLattice α] {f : ι → α} {g : ι' → α}, (∀ (i' : ι'), ∃ i, f i ≤ g i') → iInf f ≤ iInf g This theorem, `iInf_mono'`, asserts that for any type `α` that forms a complete lattice, and any two indexed sets `f` and `g` with indices of arbitrary sorts `ι` and `ι'` respectively, mapping to `α`, if for every element in the range of `g`, there exists an element in the range of `f` that is less than or equal to it, then the indexed infimum (greatest lower bound) of `f`, denoted by `iInf f`, is less than or equal to the indexed infimum of `g`, denoted by `iInf g`. More concisely: For any complete lattice `α` and indexed sets `f: ι -> α` and `g: ι' -> α` with the property that `g ι' i ≤ f ι j` for all `i ∈ ι'` and `j ∈ ι` implies `iInf f ≤ iInf g`, we have `iInf f ≤ iInf g`.
`iSup_comp_le` theorem iSup_comp_le : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {ι' : Sort u_9} (f : ι' → α) (g : ι → ι'), ⨆ x, f (g x) ≤ ⨆ y, f y This theorem states that for any complete lattice `α` and any two functions `f: ι' → α` and `g: ι → ι'`, the supremum (least upper bound) of the composition `f(g(x))` over all `x` in `ι` is less than or equal to the supremum of `f(y)` over all `y` in `ι'`. Essentially, this means that taking the supremum over the image of `g` does not produce a greater value than taking the supremum over the entire codomain of `f`. More concisely: For any complete lattice `α` and functions `f: ι' → α` and `g: ι → ι'`, the supremum of `f(g(x))` over all `x` in `ι` is less than or equal to the supremum of `f(y)` over all `y` in `ι'`.
`iSup_comm` theorem iSup_comm : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [inst : CompleteLattice α] {f : ι → ι' → α}, ⨆ i, ⨆ j, f i j = ⨆ j, ⨆ i, f i j This theorem states that for any type `α` that forms a complete lattice, and any two sorts `ι` and `ι'`, the supremum (⨆) of the function `f` where `f` takes arguments of `ι` and `ι'` does not depend on the order of supremum calculation. In other words, taking the supremum first over `ι`, then `ι'`, yields the same result as taking the supremum first over `ι'`, then `ι`. This property is known as the commutativity of the double supremum operation. More concisely: For any complete lattice `α`, the order of calculating supremums commutes: sup(_ i, sup(_ j, a)) = sup(_ j, sup(_ i, a)).
`iInf_range` theorem iInf_range : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : CompleteLattice α] {g : β → α} {f : ι → β}, ⨅ b ∈ Set.range f, g b = ⨅ i, g (f i) The theorem `iInf_range` expresses that for all types `α`, `β` and `ι` where `α` has a complete lattice structure, and for any function `g` from `β` to `α` and any function `f` from `ι` to `β`, the greatest lower bound (infimum, or `⨅`) of the range of `f` under `g` is equal to the infimum of the image of `ι` under the composition of `f` and `g`. In other words, taking the infimum over the image of the function is the same as taking the infimum over the range of the function transformed by another function. More concisely: For any complete lattice `α`, function `g : β -> α`, and function `f : ι -> β`, the infimum of `g ∘ f` equals the infimum of `f` over the range of `g`.
`IsLUB.sSup_eq` theorem IsLUB.sSup_eq : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α}, IsLUB s a → sSup s = a The theorem `IsLUB.sSup_eq` states that for any type `α` which has a structure of a complete semilattice with supremum, any set `s` of type `α`, and any element `a` of type `α`, if `a` is a least upper bound of the set `s`, then the supremum of the set `s` is equal to `a`. In other words, if `a` is the smallest element that is greater than or equal to all elements in `s`, then `a` is precisely the supremum of `s`. The theorem is a specific case from a more general theorem `isLUB_iff_sSup_eq`. More concisely: If `α` is a complete semilattice with supremum and `a` is the least upper bound of a set `s` in `α`, then `a` equals the supremum of `s`.
`sSup_range` theorem sSup_range : ∀ {α : Type u_1} {ι : Sort u_5} [inst : SupSet α] {f : ι → α}, sSup (Set.range f) = iSup f := by sorry The theorem `sSup_range` states that for any given type `α` that has a supremum (`SupSet α`), and any function `f` from a sort `ι` to `α`, the supremum of the range of `f` (`sSup (Set.range f)`) is equal to the indexed supremum of `f` (`iSup f`). In other words, the supremum of the set of all outputs of `f` is the same as the supremum found by considering `f` as an indexed family. More concisely: For any type `α` with a supremum and any function `f` from a sort `ι` to `α`, the supremum of the range of `f` equals the indexed supremum of `f`. In other words, `sSup (Set.range f) = iSup f`.
`iSup_option` theorem iSup_option : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : Option β → α), ⨆ o, f o = f none ⊔ ⨆ b, f (some b) This theorem states that for any two types `α` and `β`, where `α` is a complete lattice, and a function `f` mapping from an option of `β` to `α`, the supremum (the least upper bound or `⨆`) over all options of the function `f` is equal to the supremum of `f` at `none` and the supremum of `f` at `some b` for all `b` in `β`. Essentially, it splits the supremum over all options of `β` into two parts: one where the option is `none`, and one where the option is `some b`. More concisely: For any complete lattice `α` and a function `f` from the option type `Option β` to `α`, the supremum of `f` over all options equals the supremum of `f` at `none` plus the supremum of `f` over all `some b` in `β`.
`iSup_pos` theorem iSup_pos : ∀ {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {f : p → α} (hp : p), ⨆ (h : p), f h = f hp This theorem, `iSup_pos`, states that for any type `α` which is a complete lattice, and for any proposition `p`, and any function `f` from `p` to `α`, if `p` is true (`hp : p`), then the supremum (or least upper bound, denoted by `⨆`) of `f` over all truth values of `p` is equal to the value of `f` at `p` being true. In other words, if `p` holds, then the supremum of `f` over all instances of `p` is just `f` evaluated at `p` being true. More concisely: For any complete lattice `α` and proposition `p`, if `p` holds (`hp : p`) then the supremum of a function `f` from `p` to `α` equals `f` applied to `p`: `⨆ x in p, f x = f hp`.
`sInf_le_sInf` theorem sInf_le_sInf : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s t : Set α}, s ⊆ t → sInf t ≤ sInf s := by sorry This theorem, named `sInf_le_sInf`, states that for any type `α` that forms a complete semilattice under the infimum operation, and for any two sets `s` and `t` of this type, if `s` is a subset of `t`, then the infimum of `t` is less than or equal to the infimum of `s`. In other words, if all elements of `s` are also in `t`, then the greatest lower bound of `t` cannot be greater than the greatest lower bound of `s`. This theorem is a part of order theory in mathematics, which studies the properties of ordered sets. More concisely: For any complete semilattice `α` and sets `s` and `t` in `α` with `s ⊆ t`, the infimum of `t` is less than or equal to the infimum of `s`.
`CompleteLattice.le_sSup` theorem CompleteLattice.le_sSup : ∀ {α : Type u_9} [self : CompleteLattice α] (s : Set α), ∀ a ∈ s, a ≤ sSup s := by sorry This theorem is stating that for any type `α` that forms a complete lattice, every element `a` of any set `s` of this type is less than or equal to the supremum of the set `s`. The supremum of a set in a lattice is the least upper bound, meaning it is an element that is greater than or equal to every element in the set, and is also less than or equal to any other element that has this property. So, in simpler terms, this theorem asserts that every element in a set is less than or equal to the smallest element that is greater than or equal to everything in the set. More concisely: For any complete lattice `α` and set `s` in `α`, every element `a` in `s` is less than or equal to the supremum of `s`.
`sSup_singleton` theorem sSup_singleton : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {a : α}, sSup {a} = a This theorem states that for any type `α` that forms a complete semilattice with a supremum operation, the supremum (`sSup`) of a singleton set containing only one element `a` of type `α` is equal to `a` itself. In other words, in a complete semilattice, the least upper bound of a set with just one element is the element itself. More concisely: In a complete semilattice, the supremum of a singleton set is equal to its unique element.
`iInf_inf_eq` theorem iInf_inf_eq : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f g : ι → α}, ⨅ x, f x ⊓ g x = (⨅ x, f x) ⊓ ⨅ x, g x This theorem states that for any type `α` that forms a complete lattice, and any two functions `f` and `g` from an indexed type `ι` to `α`, the infimum (greatest lower bound) of the infimums of `f(x)` and `g(x)` over all `x` is equal to the infimum of `f(x)` taken over all `x` infimumed with the infimum of `g(x)` taken over all `x`. In mathematical terms, this theorem states that `⨅ x, f(x) ⊓ g(x) = (⨅ x, f(x)) ⊓ (⨅ x, g(x))` for all `f` and `g` from `ι` to a complete lattice `α`. This is a property regarding the interaction of the infimum operation with the meet (infimum) operation in the context of a complete lattice. More concisely: For any complete lattice `α` and functions `f` and `g` from an indexed type `ι` to `α`, the infimum of `f(x)` and `g(x)` over all `x` is equal to the infimum of `f(x)` and the infimum of `g(x)` taken individually over all `x`. (i.e., `⨅ x, f(x) ⊓ g(x) = ⨅ x, f(x) ⊓ ⨅ x, g(x)`)
`iSup_insert` theorem iSup_insert : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {s : Set β} {b : β}, ⨆ x ∈ insert b s, f x = f b ⊔ ⨆ x ∈ s, f x This theorem, `iSup_insert`, states that for any types `α` and `β` where `α` is a complete lattice, given a function `f` from `β` to `α`, a set `s` of `β`, and an element `b` of `β`, the supremum (`⨆`) of `f` over all elements `x` in the set obtained by inserting `b` into `s` is equal to the supremum of the function `f` applied to `b` and the supremum of `f` over all elements in the original set `s`. This essentially states a property of the supremum operation in the context of complete lattices and sets. More concisely: For any complete lattice `α`, function `f` from a set `β` to `α`, set `s ⊆ β`, and element `b ∈ β`, we have `⨆(f ∪ {(b, f(b))}) = ⨆(f(s)) ⊔ f(b)`, where `⊔` denotes the join (supremum) operation in `α`.
`CompleteSemilatticeInf.sInf_le` theorem CompleteSemilatticeInf.sInf_le : ∀ {α : Type u_9} [self : CompleteSemilatticeInf α] (s : Set α), ∀ a ∈ s, sInf s ≤ a This theorem states that, for any complete semilattice of type `α`, any element `a` of a given set `s` within the semilattice is greater than or equal to the infimum of the set. Here, a complete semilattice is an ordered set where any subset has an infimum (greatest lower bound). The infimum (`sInf s`) of the set `s` is the greatest element that is less than or equal to all elements of `s`. Therefore, the theorem ensures that any element `a` in the set `s` is not less than the infimum of `s`. More concisely: For any complete semilattice and any element in the semilattice, that element is greater than or equal to the infimum of the semilattice's subset to which it belongs.
`CompleteSemilatticeSup.sSup_le` theorem CompleteSemilatticeSup.sSup_le : ∀ {α : Type u_9} [self : CompleteSemilatticeSup α] (s : Set α) (a : α), (∀ b ∈ s, b ≤ a) → sSup s ≤ a The theorem `CompleteSemilatticeSup.sSup_le` states that for any type `α` which has the structure of a complete semilattice with supremum, for any set `s` of elements of this type, and for any element `a` of this type, if `a` is an upper bound of the set `s` (that is, every element `b` of `s` is less than or equal to `a`), then the supremum (the least upper bound) of the set `s` is less than or equal to `a`. More concisely: If `α` is a complete semilattice with supremum, and `a` is an upper bound of a set `s` in `α`, then `s`'s supremum is less than or equal to `a`.
`iInf_congr` theorem iInf_congr : ∀ {α : Type u_1} {ι : Sort u_5} [inst : InfSet α] {f g : ι → α}, (∀ (i : ι), f i = g i) → ⨅ i, f i = ⨅ i, g i := by sorry This theorem states that for any type `α` that has an `InfSet` instance, and for any indexing type `ι`, if we have two functions `f` and `g` from `ι` to `α`, then if every element in the image of `f` is equal to the corresponding element in the image of `g`, it follows that the infimum (`⨅`) over all `i` of `f i` is equal to the infimum over all `i` of `g i`. In other words, if two functions produce the same values, then the infimum of the values produced by these functions are the same. More concisely: If `f` and `g` are functions from an indexing type `ι` to a type `α` with an `InfSet` instance, and `f i = g i` for all `i`, then `⨅ i, f i = ⨅ i, g i`.
`iSup_le_iSup_of_subset` theorem iSup_le_iSup_of_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {s t : Set β}, s ⊆ t → ⨆ x ∈ s, f x ≤ ⨆ x ∈ t, f x This theorem states that for any types `α` and `β`, with `α` being a complete lattice, and for any function `f` from `β` to `α`, along with any sets `s` and `t` of elements of type `β`, if `s` is a subset of `t`, then the supremum (greatest lower bound) of the images of `s` under `f` is less than or equal to the supremum of the images of `t` under `f`. In mathematical terms, if `s` is a subset of `t` then `sup_{x ∈ s} f(x) ≤ sup_{x ∈ t} f(x)`. More concisely: For any complete lattice `α`, function `f` from type `β` to `α`, and sets `s` and `t` of elements in `β` where `s` is a subset of `t`, the supremum of `f` over `s` is less than or equal to the supremum of `f` over `t`. Symbolically, `sup(f(x)\|x ∈ s) ≤ sup(f(x)\|x ∈ t)`.
`sSup_apply` theorem sSup_apply : ∀ {α : Type u_9} {β : α → Type u_10} [inst : (i : α) → SupSet (β i)] {s : Set ((a : α) → β a)} {a : α}, sSup s a = ⨆ f, ↑f a This theorem states that for any type `α`, and any type `β` which is a function of `α`, given a supremum instance `SupSet` for `β i` for each `i` in `α`, for any set `s` of functions from `α` to `β a`, and for any `a` in `α`, the supremum of the set `s` applied to `a` is equal to the supremum over all functions `f` of `f` applied to `a`. This theorem utilizes the concept of supremum in the setting of set of functions, and it relates the supremum of a set of functions to the supremum of the values of these functions at a particular point. More concisely: For any type `α` and any function type `β -> α -> Type`, given a supremum `s` for each `β i` over `i ∈ α`, the supremum of a set `s` of functions `f : α -> β a` is equal to the function `sup : β a` such that for all `g : α -> β a`, `sup ≤ g`, and for all `i ∈ α`, `sup i = (sup a) i`.
`iSup_exists` theorem iSup_exists : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {p : ι → Prop} {f : Exists p → α}, ⨆ (x : Exists p), f x = ⨆ i, ⨆ (h : p i), f ⋯ This theorem, `iSup_exists`, states that for any type `α` that forms a complete lattice, and for any predicate `p` over some index type `ι`, there is an equivalence between the supremum over all elements satisfying the predicate `p` and the corresponding function `f` applied on their existence proofs, and the supremum over all indices `i` with the second supremum over all elements satisfying the predicate `p(i)`. It effectively shows that the supremum operation is invariant under the proof of existence. More concisely: For any complete lattice `α` and predicate `p` over an index type `ι`, the function `f` that maps an element `x` to its existence proof returns the supremum of elements satisfying `p` if and only if it is the supremum of the second supremum of elements `i` with `p(i)`.
`Prod.snd_iInf` theorem Prod.snd_iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : InfSet α] [inst_1 : InfSet β] (f : ι → α × β), (iInf f).2 = ⨅ i, (f i).2 The theorem `Prod.snd_iInf` states that for any types `α`, `β`, and `ι`, given an infimum set structure on `α` and `β`, and a function `f : ι → α × β` (i.e., a function that maps elements from `ι` to pairs of elements in `α` and `β`), the second component of the infimum of the function `f` (that is, `(iInf f).2`) is equal to the infimum over all `i` of the second component of `f(i)` (which is represented by `⨅ i, (f i).2`). In other words, it extracts the infimum of the second components of the pairs generated by the function `f` over the index set `ι`. More concisely: For any functions `f : ι → α × β`, the second component of the infimum of `f` equals the infimum of the second components of `f(i)` for all `i` in the index set.
`isGLB_sInf` theorem isGLB_sInf : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] (s : Set α), IsGLB s (sInf s) This theorem states that for any type `α`, which is a complete semilattice with respect to the infimum operation, and for any set `s` of type `α`, the infimum of `s` (denoted as `sInf s`) is a greatest lower bound of set `s`. In other words, the infimum of a set in a complete semilattice is the largest element that is less than or equal to all elements of the set. More concisely: In a complete semilattice, the infimum of a set is its greatest lower bound.
`OrderIso.map_iInf` theorem OrderIso.map_iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β) (x : ι → α), f (⨅ i, x i) = ⨅ i, f (x i) This theorem, `OrderIso.map_iInf`, states that for any two complete lattices `α` and `β`, and for any function from an arbitrary type `ι` to `α`, the image under an order isomorphism `f` of the greatest lower bound (infimum) of `x` over all `ι` is equal to the greatest lower bound of the image of `x` under `f` over all `ι`. In mathematical terms, it says that if `f` is an order isomorphism between `α` and `β`, then `f(inf i, x(i)) = inf i, f(x(i))`, where `inf` denotes the greatest lower bound (infimum). More concisely: For any order isomorphism `f` between complete lattices `α` and `β` and any function `x : ι → α`, `f(inf ι, x i) = inf ι, f(x i)`.
`iSup_congr` theorem iSup_congr : ∀ {α : Type u_1} {ι : Sort u_5} [inst : SupSet α] {f g : ι → α}, (∀ (i : ι), f i = g i) → ⨆ i, f i = ⨆ i, g i := by sorry This theorem, `iSup_congr`, states that for all types `α` and `ι`, where `α` has a supremum operation (`SupSet`), if we have two functions `f` and `g` from `ι` to `α`, then if every element `i` in `ι` maps to the same element in `α` under both `f` and `g` (i.e., `f i = g i` for all `i` in `ι`), the supremum over all values of `f i` is equal to the supremum over all values of `g i`. In other words, the supremum is invariant under pointwise equal functions. More concisely: If `f` and `g` are pointwise equal functions from an index set `ι` to a type `α` with a supremum operation, then `SupSet (f ↥ ι) = SupSet (g ↥ ι)`.
`iSup_eq_top` theorem iSup_eq_top : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLinearOrder α] (f : ι → α), iSup f = ⊤ ↔ ∀ b < ⊤, ∃ i, b < f i := by sorry This theorem states that for any type `α` that has a complete linear order structure and any function `f` from an index type `ι` to `α`, the indexed supremum of `f` (denoted `iSup f`) equals the greatest element (`⊤`) if and only if for every element `b` that is less than `⊤`, there exists an index `i` such that `b` is less than `f(i)`. In other words, the supremum of the range of `f` is the greatest element if and only if for any value less than this greatest element, we can find an index where the function value at this index is more than the given value. More concisely: For a complete linear order type `α` and any function `f : ι → α`, the indexed supremum `iSup f` equals the greatest element `⊤` if and only if for all `b` < `⊤`, there exists an `i` such that `f(i)` > `b`.
`iSup_eq_bot` theorem iSup_eq_bot : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {s : ι → α}, iSup s = ⊥ ↔ ∀ (i : ι), s i = ⊥ This theorem, `iSup_eq_bot`, states that for any type `α` that forms a complete lattice, and any function `s` from some type `ι` to `α`, the supremum of the function `s` (denoted by `iSup s`) equals the bottom element of the lattice (denoted by `⊥`) if and only if every element `i` of type `ι` maps to the bottom of the lattice under the function `s` (i.e., `s i = ⊥` for all `i`). In other words, the supremum of the range of `s` is the smallest element of the lattice if and only if all values in the range of `s` are the smallest element of the lattice. More concisely: For any complete lattice `α` and function `s` from a type `ι` to `α`, `iSup s = ⊥` if and only if `s i = ⊥` for all `i ∈ ι`. (The supremum of a function `s` equals the bottom element of the lattice if and only if all images under `s` are the bottom element.)
`iSup_sigma` theorem iSup_sigma : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {p : β → Type u_9} {f : Sigma p → α}, ⨆ x, f x = ⨆ i, ⨆ j, f ⟨i, j⟩ This theorem states that for any types `α` and `β`, where `α` is a complete lattice, and any function `f` from a dependent pair (Sigma type) `p` of `β` to `α`, the supremum (maximum) value of `f` over all `x` (which is a dependent pair of `β` and `p`) is equal to the nested supremum of `f` over all `i` and `j`, where `i` is of type `β` and `j` is of type `p i`. In other words, this theorem establishes an equivalence between a direct supremum over a dependent pair and a nested supremum over each component of the pair. More concisely: For any complete lattice α and function f from a dependent Sigma type p of β to α, the supremum of f over all x (dependent pairs i, j of β and p) is equal to the nested supremum over all i in β of the supremum of f over j (p i).
`CompleteLattice.bot_le` theorem CompleteLattice.bot_le : ∀ {α : Type u_9} [self : CompleteLattice α] (x : α), ⊥ ≤ x This theorem states that for any element `x` within a complete lattice of type `α`, the bottom element of the lattice is always less than or equal to `x`. In the language of lattice theory, this is expressing the property that the bottom element (often denoted as `⊥`) is a lower bound for any element in the lattice. More concisely: In any complete lattice, the bottom element is a lower bound for all elements.
`sSup_le_iff` theorem sSup_le_iff : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α}, sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a This theorem states that for any type `α` that forms a complete semilattice with respect to the supremum operation and for any set `s` of elements of type `α` and for any element `a` of type `α`, the supremum of set `s` is less than or equal to `a` if and only if every element `b` in set `s` is less than or equal to `a`. In other words, the largest element of `s` (its supremum) is not greater than `a` precisely when each element of `s` is not greater than `a`. More concisely: For any complete semilattice `α` and any set `s` of elements from `α` with supremum `sup s` and any element `a` in `α`, `sup s ≤ a` if and only if `x ≤ a` for all `x` in `s`.
`le_iInf` theorem le_iInf : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f : ι → α} {a : α}, (∀ (i : ι), a ≤ f i) → a ≤ iInf f The theorem `le_iInf` states that for any type `α` that forms a complete lattice, any function `f` from some index set `ι` to `α`, and any element `a` of `α`, if `a` is less than or equal to every value `f(i)` for all `i` in `ι`, then `a` is less than or equal to the indexed infimum of the function `f`. In other words, if `a` is less than or equal all values of `f`, then `a` is less than or equal to the greatest lower bound of the range of `f`. More concisely: For any complete lattice `α`, if `a ≤ f(i)` for all `i` in the index set `ι`, then `a ≤ ∧ⁱ i.in f` (the infimum of `f`).
`iSup_range` theorem iSup_range : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : CompleteLattice α] {g : β → α} {f : ι → β}, ⨆ b ∈ Set.range f, g b = ⨆ i, g (f i) This theorem states that for any types `α`, `β`, and `ι`, given a complete lattice structure on `α` and functions `g: β → α` and `f: ι → β`, the supremum (⨆, a generalization of the maximum for sets that may not have a greatest element) of the function `g` over the range of `f` is equal to the supremum of `g ∘ f` over `ι`. In other words, it doesn't matter whether we first apply `f` to each element of `ι` and then find the supremum of `g` values, or first find the supremum over the range of `f` and then apply `g`. More concisely: For any complete lattices `α`, `β`, and `ι`, and functions `g: β → α` and `f: ι → β`, the supremum of `g ∘ f` over `ι` equals the supremum of `g` over the range of `f`.
`iSup_mono'` theorem iSup_mono' : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [inst : CompleteLattice α] {f : ι → α} {g : ι' → α}, (∀ (i : ι), ∃ i', f i ≤ g i') → iSup f ≤ iSup g The theorem `iSup_mono'` states that for any two types `α` and `ι` (respectively `ι'`) with `α` being a complete lattice, and any two functions `f : ι → α` and `g : ι' → α`, if for every element of `ι` there exists an element in `ι'` such that the value of `f` at that element is less than or equal to the value of `g` at the corresponding element, then the supremum (greatest lower bound) of the range of `f` is less than or equal to the supremum of the range of `g`. In other words, if `f` is pointwise less than or equal to `g`, then the supremum of `f` is less than or equal to the supremum of `g`. More concisely: If `α` is a complete lattice and `f : ι → α` is pointwise less than or equal to `g : ι' → α`, then `sup (range f) ≤ sup (range g)`.
`iInf_emptyset` theorem iInf_emptyset : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α}, ⨅ x ∈ ∅, f x = ⊤ := by sorry This theorem states that for any type `α` that forms a complete lattice and any function `f` from type `β` to `α`, the infimum (greatest lower bound) of `f x` for all `x` in the empty set is the top element (⊤) of the lattice. In other words, if we take the infimum of a function applied to no elements at all, we get the greatest possible value in the lattice. More concisely: For any complete lattice `α` and function `f` from type `β` to `α`, the infimum of `f x` over the empty set is the top element `⊤` of the lattice.
`le_iSup₂` theorem le_iSup₂ : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [inst : CompleteLattice α] {f : (i : ι) → κ i → α} (i : ι) (j : κ i), f i j ≤ ⨆ i, ⨆ j, f i j This theorem, `le_iSup₂`, states that for any complete lattice `α`, and any function `f` which maps an index `i` of type `ι` and another index `j` of type `κ i` to an element of `α`, the value `f i j` for any specific `i` and `j` is less than or equal to the supremum (or least upper bound) over all possible `i` and `j` of `f i j`. This theorem essentially states that any specific output of the function `f` is less than or equal to the maximum possible output of the function `f` over all inputs. More concisely: For any complete lattice `α` and function `f` from the product type `ι × κ` to `α`, `∀ i ∈ ι ∀ j ∈ κ i, f i j ≤ ⨜ (i, j) in ι × κ, f i j)`.
`iSup_const_mono` theorem iSup_const_mono : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [inst : CompleteLattice α] {a : α}, (ι → ι') → ⨆ x, a ≤ ⨆ x, a := by sorry This theorem states that for any type `α` that forms a complete lattice, and any element `a` of `α`, the supremum of the set of elements `a` is less than or equal to itself. This is true regardless of the indexing types `ι` and `ι'`, and any function from `ι` to `ι'`. In simpler terms, it says that the supremum of a constant sequence in a complete lattice is less than or equal to the constant itself. More concisely: For any complete lattice `α` and its element `a`, the supremum of the singleton set `{a}` is less than or equal to `a`.
`inf_eq_iInf` theorem inf_eq_iInf : ∀ {α : Type u_1} [inst : CompleteLattice α] (x y : α), x ⊓ y = ⨅ b, bif b then x else y := by sorry This theorem states that for any complete lattice `α` and any two elements `x` and `y` from `α`, the infimum of `x` and `y` (denoted as `x ⊓ y`) is equal to the infimum (denoted as `⨅ b`) over all boolean values `b` such that if `b` is true, then the value is `x`, else the value is `y`. That is, the smallest element that's less than or equal to both `x` and `y` is the same as the smallest element when comparing `x` and `y` as options determined by boolean value `b`. More concisely: For any complete lattice `α` and elements `x, y ∈ α`, the infimum `x ⊓ y` equals the greatest lower bound over all boolean values `b` such that `x = b ⟶ x` and `y = ¬b ⟶ y`. (Here, `⟶` denotes material implication and `¬` denotes boolean negation.)
`Function.Surjective.iSup_congr` theorem Function.Surjective.iSup_congr : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [inst : SupSet α] {f : ι → α} {g : ι' → α} (h : ι → ι'), Function.Surjective h → (∀ (x : ι), g (h x) = f x) → ⨆ x, f x = ⨆ y, g y The theorem `Function.Surjective.iSup_congr` states that for any types `α`, `ι`, and `ι'`, given a `SupSet` instance for `α`, and functions `f : ι → α`, `g : ι' → α`, and a surjective function `h : ι → ι'`, if for all `x` in `ι`, `g (h x)` equals `f x`, then the supremum of the image of `f` equals the supremum of the image of `g`. Here, `⨆ x, f x` means the supremum (greatest element) of the image of `f`, and similarly for `g`. This theorem essentially says that a surjective transformation of the indexing set of a supremum doesn't change the supremum, as long as the function values are preserved under the transformation. More concisely: If `f : ι → α` and `g : ι' → α` are functions with `ι` and `ι'` having a `SupSet` instance, and `h : ι → ι'` is surjective such that `g (h x) = f x` for all `x` in `ι`, then `⨆ x, f x = ⨆ x, g x`.
`iInf_image` theorem iInf_image : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {γ : Type u_9} {f : β → γ} {g : γ → α} {t : Set β}, ⨅ c ∈ f '' t, g c = ⨅ b ∈ t, g (f b) The theorem `iInf_image` states that for any types `α`, `β`, and `γ` where `α` is a complete lattice, and for any functions `f` mapping from `β` to `γ` and `g` mapping from `γ` to `α`, and for any set `t` of type `β`, the infimum (greatest lower bound, denoted by `⨅`) over the image of the set `t` under the function `f`, of `g(c)` where `c` belongs to the image set, is equal to the infimum over the set `t`, of `g(f(b))` where `b` belongs to the set `t`. In other words, applying the function `f` before or after taking the infimum (with respect to `g`) does not change the result. More concisely: For any complete lattice α, functions f: β → γ and g: γ → α, and set t ∈ β, the infimum (g ∘ f)(t) = (∧ x ∈ t. g(f(x))) where ∧ denotes the infimum over the set.
`iSup_eq_of_forall_le_of_forall_lt_exists_gt` theorem iSup_eq_of_forall_le_of_forall_lt_exists_gt : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {b : α} {f : ι → α}, (∀ (i : ι), f i ≤ b) → (∀ w < b, ∃ i, w < f i) → ⨆ i, f i = b This theorem states that for a given type `α` endowed with a CompleteLattice structure, a function `f` mapping from any type `ι` to `α`, and an element `b` of type `α`, if `b` is larger than or equal to all values of `f i` for all `i` of type `ι` and there is no `w` smaller than `b` for which there isn't a corresponding `i` such that `w` is less than `f i`, then `b` is the supremum of the set of all `f i`. Essentially, it provides a rule for proving the supremum of a set in the context of a CompleteLattice. More concisely: In a complete lattice, an element is the supremum if and only if it is greater than or equal to every other element and there is no smaller element not belonging to the image of some element under the lattice homomorphism.
`iSup_iSup_eq_right` theorem iSup_iSup_eq_right : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {b : β} {f : (x : β) → b = x → α}, ⨆ x, ⨆ (h : b = x), f x h = f b ⋯ This theorem states that for any types `α` and `β`, given a complete lattice structure on `α`, a value `b` of type `β`, and a function `f` from `β` (whose equality to `b` is ensured by a proof `h`) to `α`, the supremum over all `x` of the supremum over all proofs `h` of `b = x` for `f x h` is equal to `f b ⋯`. Essentially, it's saying that the double supremum of `f` over all `x` and proofs of `b = x` collapses to applying `f` directly to `b` and some unspecified values (represented by `⋯`). More concisely: For any complete lattice `α`, any `β`, a function `f` from `β` to `α`, and `b` in `β` with a proof `h` of `b = b`, the double supremum of `f x h` over all `x` and proofs `h` of `b = x` equals `f b`.
`iInf_pos` theorem iInf_pos : ∀ {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {f : p → α} (hp : p), ⨅ (h : p), f h = f hp This theorem, `iInf_pos`, states that for any type `α` that forms a complete lattice, given a proposition `p` and a function `f` from `p` to `α`, for any instance `hp` where `p` holds true, the infimum (greatest lower bound) over all elements `h` for which `p` holds, of `f(h)`, is equal to `f(hp)`. In other words, it asserts that the infimum of the function values for all instances of the proposition is the function value at the particular instance `hp`. More concisely: For any complete lattice `α`, function `f` from a proposition `p` to `α`, and instance `hp` of `p`, the infimum of `f(h)` over all `h` with `p(h)` is equal to `f(hp)`.
`iSup_or` theorem iSup_or : ∀ {α : Type u_1} [inst : CompleteLattice α] {p q : Prop} {s : p ∨ q → α}, ⨆ (x : p ∨ q), s x = (⨆ (i : p), s ⋯) ⊔ ⨆ (j : q), s ⋯ This theorem states that for any type `α` that forms a complete lattice, and for any propositions `p` and `q`, and a function `s` from the disjunction `p ∨ q` to `α`, the supremum (or least upper bound) of `s` over all `p ∨ q` is equal to the join (or supremum) of the supremum of `s` over all `p` and the supremum of `s` over all `q`. This captures the idea that the greatest element of a set determined by either `p` or `q` is the greatest element among those determined by `p` and those determined by `q`, combined. More concisely: For any complete lattice `α` and functions `s` from `p ∨ q` to `α`, the supremum of `s` over `p ∨ q` equals the join of the supremum of `s` over `p` and the supremum of `s` over `q`.
`biInf_mono` theorem biInf_mono : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f : ι → α} {p q : ι → Prop}, (∀ (i : ι), p i → q i) → ⨅ i, ⨅ (_ : q i), f i ≤ ⨅ i, ⨅ (_ : p i), f i This theorem states that for any completely ordered lattice of type α and any function `f` from `ι` to `α`, if `p` is a predicate on `ι` and `q` is another predicate on `ι` such that every element that satisfies `p` also satisfies `q`, then the infimum of `f` over all elements satisfying `q` is greater than or equal to the infimum of `f` over all elements satisfying `p`. The infimum is a notion of the minimal value that `f` can take, considering the constraints posed by `q` and `p`. In simple terms, if `q` is a broader condition than `p` (i.e., more elements satisfy `q`), then the smallest value that `f` can take under `q` cannot be smaller than the smallest value under `p`. More concisely: For any completely ordered lattice α and function f from ι to α, if p and q are predicates on ι with p implying q, then the infimum of f over elements satisfying q is greater than or equal to the infimum of f over elements satisfying p.
`le_sInf` theorem le_sInf : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α}, (∀ b ∈ s, a ≤ b) → a ≤ sInf s The theorem `le_sInf` states that for any type `α` that has an instance of a complete semilattice with an infimum (`CompleteSemilatticeInf α`), for any set `s` of this type `α`, and for any element `a` of type `α`, if `a` is less than or equal to every element `b` in the set `s`, then `a` is less than or equal to the infimum (`sInf`) of the set `s`. In simpler terms, if `a` is less than or equal to all elements of a set, then it is also less than or equal to the greatest lower bound of the set. More concisely: If `α` is a complete semilattice with an infimum and `a` is in `α` such that `a ≤ b` for all `b` in a set `s` of `α`, then `a ≤ sInf s`.
`iSup_image` theorem iSup_image : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {γ : Type u_9} {f : β → γ} {g : γ → α} {t : Set β}, ⨆ c ∈ f '' t, g c = ⨆ b ∈ t, g (f b) The theorem `iSup_image` states that for any types `α`, `β`, `γ`, where `α` is a complete lattice, and any functions `f` from `β` to `γ` and `g` from `γ` to `α`, and a set `t` of type `β`, the supremum (denoted by `⨆`) of the image of `t` under `f`, after applying `g`, is equal to the supremum of `t`, after applying `g` composed with `f`. In other words, it shows that the order of taking supremum and applying the function composition `g ∘ f` can be swapped. More concisely: For any complete lattice α, functions f : β → γ and g : γ → α, and set t ⊆ β, the image of the supremum of t under g ∘ f is equal to the supremum of the image of t under f, then applied to the supremum of the resulting values under g.
`Function.Surjective.iInf_congr` theorem Function.Surjective.iInf_congr : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [inst : InfSet α] {f : ι → α} {g : ι' → α} (h : ι → ι'), Function.Surjective h → (∀ (x : ι), g (h x) = f x) → ⨅ x, f x = ⨅ y, g y The theorem `Function.Surjective.iInf_congr` states that for any types `α`, `ι`, and `ι'`, where `α` has an infimum defined, and any functions `f : ι → α` and `g : ι' → α`, if there exists a function `h : ι → ι'` which is surjective, and for each `x : ι`, `g (h x)` equals `f x`, then the infimum of the values of `f` over all `x` is equal to the infimum of the values of `g` over all `y`. In simpler terms, it says that if we can rearrange the inputs to the functions `f` and `g` such that they give the same outputs, then the infimum of `f`'s values is the same as the infimum of `g`'s values. More concisely: If `f : ι → α` and `g : ι' → α` have the same values for the images of a surjective function `h : ι → ι'`, then the infimum of `f` is equal to the infimum of `g`.
`CompleteLattice.sInf_le` theorem CompleteLattice.sInf_le : ∀ {α : Type u_9} [self : CompleteLattice α] (s : Set α), ∀ a ∈ s, sInf s ≤ a := by sorry This theorem, `CompleteLattice.sInf_le`, states that for any set `s` in the context of a `CompleteLattice` of type `α`, any element `a` belonging to this set `s` will be greater than or equal to the infimum (`sInf`) of the set. In other words, the least element in a complete lattice, when ordered by the lattice operations, is less than or equal to every element in the set. More concisely: For any set in a complete lattice and any element in that set, the infimum is less than or equal to that element.
`iSup_union` theorem iSup_union : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {s t : Set β}, ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x This theorem states that for any types `α` and `β`, with `α` being a complete lattice, and any function `f` of type `β → α`, and any sets `s` and `t` of type `Set β`, the supremum of `f(x)` where `x` is in the union of `s` and `t` is equal to the supremum of `f(x)` where `x` is in `s` joined with the supremum of `f(x)` where `x` is in `t`. In mathematical notation, this can be written as $\sup_{x \in (s \cup t)} f(x) = \sup_{x \in s} f(x) \cup \sup_{x \in t} f(x)$. More concisely: For any complete lattice `α`, function `f` from type `β` to `α`, and sets `s` and `t` of type `Set β`, the supremum of `f(x)` over `x` in `s ∪ t` equals the join (supremum) of the supremums of `f(x)` over `x` in `s` and `f(x)` over `x` in `t`. In Lean notation: `sup (f <$> (s ++ t)) = sup (f <$> s) ⊔ sup (f <$> t)`.
`le_iSup` theorem le_iSup : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] (f : ι → α) (i : ι), f i ≤ iSup f := by sorry The theorem `le_iSup` asserts that for any type `α` which forms a complete lattice, for any function `f` from a type `ι` to `α`, and for any element `i` of `ι`, the value of the function `f` at `i` is less than or equal to the indexed supremum of the function `f`. In other words, it states that any individual element of the function `f` is not greater than the supremum of all elements in the range of `f`. More concisely: For any complete lattice `α` and function `f` from a type `ι` to `α`, the value `f i` is less than or equal to the supremum of `f` for all `i` in `ι`.
`Function.Surjective.iSup_comp` theorem Function.Surjective.iSup_comp : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [inst : SupSet α] {f : ι → ι'}, Function.Surjective f → ∀ (g : ι' → α), ⨆ x, g (f x) = ⨆ y, g y The theorem `Function.Surjective.iSup_comp` states that for any types `α`, `ι`, and `ι'`, given a supremum set on `α` and a function `f` from `ι` to `ι'` which is surjective (that is, every element of `ι'` is the image of some element of `ι` under `f`), then for any function `g` from `ι'` to `α`, the supremum of `g` composed with `f` over all `x` in `ι` is equal to the supremum of `g` over all `y` in `ι'`. In other words, surjectivity of the function `f` ensures that applying `f` to the elements of `ι` before taking the supremum does not change the final supremum value in the context of the function `g`. More concisely: For any types `α`, `ι`, `ι'`, a supremum `s` on `α` from `ι`, and a surjective function `f` from `ι` to `ι'`, the supremum of `g ∘ f` over `ι` equals the supremum of `g` over `ι'`.
`iInf_eq_of_forall_ge_of_forall_gt_exists_lt` theorem iInf_eq_of_forall_ge_of_forall_gt_exists_lt : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f : ι → α} {b : α}, (∀ (i : ι), b ≤ f i) → (∀ (w : α), b < w → ∃ i, f i < w) → ⨅ i, f i = b This theorem states that for any type `α` that forms a complete lattice and a function `f` from some index type `ι` to `α`, if `b` is an element of `α` that is less than or equal to every output of `f` and there does not exist an element `w` of `α` that is strictly greater than `b` but less than any output of `f`, then `b` is the greatest lower bound (infimum) of the range of `f`. This theorem provides an introduction rule for proving that an element is the infimum in a complete lattice. It also references a similar rule for conditionally complete lattices. More concisely: If `α` is a complete lattice and `f:` `ι` `→` `α` is a function with `b` as its greatest lower bound (infimum) such that for all `x` in the range of `f`, `b ≤ x` and there is no `w` in `α` with `w < x` and `w > b`, then `b` is the infimum of `f`.
`iInf_and` theorem iInf_and : ∀ {α : Type u_1} [inst : CompleteLattice α] {p q : Prop} {s : p ∧ q → α}, iInf s = ⨅ (h₁ : p), ⨅ (h₂ : q), s ⋯ := by sorry This theorem states that for any type `α` that forms a complete lattice, and for any propositions `p` and `q`, the indexed infimum (i.e., the greatest lower bound) of a function `s` that maps from the conjunction `p ∧ q` to `α` is equal to the infimum over `h₁` in `p` and `h₂` in `q` of `s`. In other words, it describes taking the infimum first over all truth assignments that make `p` true, and then over all truth assignments that make `q` true, and this gives the same result as taking the infimum directly over all truth assignments that make both `p` and `q` true. More concisely: For any complete lattice `α` and propositions `p` and `q`, the infimum of a function `s` from `p ∧ q` to `α` equals the infimum over `h₁ in p` and `h₂ in q` of `s(h₁, h₂)`.
`iInf_iInf_eq_left` theorem iInf_iInf_eq_left : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {b : β} {f : (x : β) → x = b → α}, ⨅ x, ⨅ (h : x = b), f x h = f b ⋯ This theorem, named `iInf_iInf_eq_left`, states that for any types `α` and `β`, where `α` is a Complete Lattice, and for any value `b` of type `β` and any function `f` from type `β` which equates to `b` to type `α`, the infimum (denoted by `⨅`) over all `x` of the infimum over all `h` where `h` is the equality `x = b` of `f(x, h)` is equal to `f(b, ...)`. In simpler terms, it's saying that in a Complete Lattice, the infimum of the infimum of a certain function `f` over all `x` equal to `b` is equal to the function evaluated at `b`. More concisely: In a complete lattice, for any function from the lattice to itself, the infimum of the infima over all elements equal to a given one is equal to the image of that element under the function.
`iSup_le` theorem iSup_le : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f : ι → α} {a : α}, (∀ (i : ι), f i ≤ a) → iSup f ≤ a The theorem `iSup_le` states that for any type `α` that is a complete lattice, any function `f` from an arbitrary type `ι` to `α`, and any value `a` of type `α`, if every value `f(i)` for all `i` in `ι` is less than or equal to `a`, then the indexed supremum of the function `f`, denoted as `iSup f`, is also less than or equal to `a`. In other words, if all the values of a function are below a specific value, then their supremum (greatest value) is also below or equal to that specific value. More concisely: For any complete lattice α and function f from type ι to α, if for all i in ι, f(i) ≤ a, then iSup f ≤ a.
`CompleteSemilatticeInf.le_sInf` theorem CompleteSemilatticeInf.le_sInf : ∀ {α : Type u_9} [self : CompleteSemilatticeInf α] (s : Set α) (a : α), (∀ b ∈ s, a ≤ b) → a ≤ sInf s The theorem `CompleteSemilatticeInf.le_sInf` states that for any type `α` that forms a complete semilattice with an infimum operation, and any set `s` of elements of this type, if some element `a` of the type is a lower bound for the set (meaning that `a` is less than or equal to every element in `s`), then `a` is also less than or equal to the infimum (greatest lower bound) of the set `s`. More concisely: If `α` is a type with a complete semilattice structure and infimum operation, and `a` is a lower bound for a set `s` in `α`, then `a` is less than or equal to the infimum of `s`.
`sInf_empty` theorem sInf_empty : ∀ {α : Type u_1} [inst : CompleteLattice α], sInf ∅ = ⊤ This theorem states that for any type `α` that forms a complete lattice, the infimum (or greatest lower bound) of an empty set is the top element (`⊤`). In other words, in the context of a complete lattice, the smallest element of an empty set is the largest possible element in the lattice. More concisely: In a complete lattice, the infimum of the empty set is the top element.
`sSup_eq_bot` theorem sSup_eq_bot : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, sSup s = ⊥ ↔ ∀ a ∈ s, a = ⊥ This theorem, `sSup_eq_bot`, states that for any given type `α`, which is a complete lattice, and any set `s` of type `α`, the supremum of set `s`, denoted as `sSup s`, is equal to the bottom element of the lattice (represented as `⊥` in Lean 4) if and only if all elements `a` in set `s` are equal to the bottom element of the lattice. In other words, the greatest lower bound of a set in a complete lattice is the lowest element of the lattice if and only if every element in the set is also the lowest element of the lattice. More concisely: For any complete lattice `α` and set `s` in `α`, `sSup s = ⊥` if and only if all elements in `s` are `⊥`.
`le_iSup_inf_iSup` theorem le_iSup_inf_iSup : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] (f g : ι → α), ⨆ i, f i ⊓ g i ≤ (⨆ i, f i) ⊓ ⨆ i, g i This theorem, `le_iSup_inf_iSup`, states that for any type `α` that forms a complete lattice, and for any two functions `f` and `g` from some index type `ι` to `α`, the supremum (i.e., least upper bound) over the index `i` of the infimum (greatest lower bound) of `f i` and `g i` is less than or equal to the infimum of the suprema of `f i` and `g i`. In mathematical terms, it's saying that `⨆ i, (f i ⊓ g i) ≤ (⨆ i, f i) ⊓ (⨆ i, g i)`. More concisely: For any complete lattice `α` and functions `f` and `g` from an index type `ι` to `α`, the infimum of the suprema of `f(i)` and `g(i)` over all `i` is greater than or equal to the supremum of the infima of `f(i)` and `g(i)` for all `i`. (The original statement is equivalent but negated and has a different focus on bounds.)
`sInf_range` theorem sInf_range : ∀ {α : Type u_1} {ι : Sort u_5} [inst : InfSet α] {f : ι → α}, sInf (Set.range f) = iInf f := by sorry The theorem `sInf_range` asserts that for any function `f` from a type `ι` to another type `α` (where `α` is equipped with an infimum operation over sets), the supremum of the image of `f` (i.e., `sInf (Set.range f)`) is equal to the indexed infimum of `f` (i.e., `iInf f`). In other words, taking the supremum of the set consisting of all values `f` can take (the range of `f`), is the same as taking the infimum of `f` itself. More concisely: For any function from a type to a type equipped with an infimum operation, the supremum of the function's image is equal to the indexed infimum of the function.
`sSup_empty` theorem sSup_empty : ∀ {α : Type u_1} [inst : CompleteLattice α], sSup ∅ = ⊥ This theorem states that for any type `α` that is a complete lattice, the supremum (or greatest lower bound) of an empty set is the minimal element (`⊥`). In other words, in the context of any complete lattice, when we attempt to find the supremum of no elements, we yield the smallest possible value within the lattice. More concisely: In a complete lattice, the supremum of an empty set equals the minimal element.
`sSup_pair` theorem sSup_pair : ∀ {α : Type u_1} [inst : CompleteLattice α] {a b : α}, sSup {a, b} = a ⊔ b This theorem states that for any complete lattice of type α, the supremum of the set containing just two elements a and b is the same as the join of a and b. Here, `⊔` represents the join operation in lattice theory, which is the least upper bound of a and b. The complete lattice is a partially ordered set in which every subset has a least upper bound (supremum) and a greatest lower bound (infimum). More concisely: In a complete lattice, the supremum of the set {a, b} equals the join of a and b.
`iSup_plift_down` theorem iSup_plift_down : ∀ {α : Type u_1} {ι : Sort u_5} [inst : SupSet α] (f : ι → α), ⨆ i, f i.down = ⨆ i, f i := by sorry This theorem states that for any type `α` with a `SupSet` instance and a function `f` from sort `ι` to `α`, the supremum of the results of applying `f` to the "down" version of elements of `ι` is equal to the supremum of the results of applying `f` directly to elements of `ι`. In mathematical terms, this can be expressed as: for any function `f : ι → α`, the following equality holds: `sup {f(i.down) \| i in ι} = sup {f(i) \| i in ι}`. More concisely: For any function `f` from a type `ι` to a type `α` with a `SupSet` instance, the supremum of `f` applied to the "down" version of `ι`'s elements equals the supremum of `f` applied to the elements themselves: `sup (map down (f ∘ i) i) = sup (f i)`.
`OrderIso.map_sSup_eq_sSup_symm_preimage` theorem OrderIso.map_sSup_eq_sSup_symm_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β) (s : Set α), f (sSup s) = sSup (⇑f.symm ⁻¹' s) The theorem `OrderIso.map_sSup_eq_sSup_symm_preimage` states that for any complete lattices `α` and `β`, and for any order isomorphism `f` from `α` to `β`, and for any set `s` of elements in `α`, the supremum (`sSup`) of `s` under the isomorphism `f` is equal to the supremum of the preimage of `s` under the inverse of the isomorphism `f`. In other words, applying the isomorphism `f` to the supremum of a set `s` in the domain lattice is the same as taking the supremum of the mapped set in the range lattice. More concisely: For any complete lattices α and β, and order isomorphism f between them, the supremum of the preimage of a subset under the inverse of f is equal to the image of the supremum under f.
`iInf_and'` theorem iInf_and' : ∀ {α : Type u_1} [inst : CompleteLattice α] {p q : Prop} {s : p → q → α}, ⨅ (h₁ : p), ⨅ (h₂ : q), s h₁ h₂ = ⨅ (h : p ∧ q), s ⋯ ⋯ This theorem, `iInf_and'`, is about the concept of infimum in complete lattices. More specifically, it asserts that for any type `α` that is a complete lattice, and any propositions `p` and `q`, as well as any function `s` that takes proof of `p` and `q` to produce an instance of `α`, the infimum over `h₁ : p` and `h₂ : q`, i.e., all pairs of proofs of `p` and `q`, is equal to the infimum over `h : p ∧ q`, i.e., all proofs of the conjunction `p ∧ q`. This theorem is especially useful for rewriting expressions involving infimums over conjunctions. More concisely: In a complete lattice, the infimum of all pairs of proofs of `p` and `q` is equal to the infimum of all proofs of `p ∧ q`.
`biSup_prod` theorem biSup_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_4} [inst : CompleteLattice α] {f : β × γ → α} {s : Set β} {t : Set γ}, ⨆ x ∈ s ×ˢ t, f x = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b) The theorem `biSup_prod` states that for any types `α`, `β`, and `γ`, where `α` is a complete lattice, and for any function `f` from the product of `β` and `γ` to `α`, and for any sets `s` of `β` and `t` of `γ`, the supremum (⨆, also known as the least upper bound or join) of `f` over the cartesian product of the sets `s` and `t` is equal to the supremum of the supremums of `f` applied to pairs `(a, b)` where `a` is an element of `s` and `b` is an element of `t`. This theorem demonstrates a property of supremums over product sets in the context of complete lattices. More concisely: For any complete lattice α, function f from the product of sets β × γ to α, and sets s ⊆ β and t ⊆ γ, the supremum of f over s × t equals the supremum of the supremums of f over pairs (a, b) with a ∈ s and b ∈ t.
`sSup_eq_iSup'` theorem sSup_eq_iSup' : ∀ {α : Type u_1} [inst : SupSet α] (s : Set α), sSup s = ⨆ a, ↑a The theorem `sSup_eq_iSup'` states that for any type 'α' and for any set 's' of this type, where 'α' is equipped with a supremum operation (expressed by the `SupSet α` typeclass), the supremum of the set 's' (denoted by `sSup s`) is equal to the supremum over all elements 'a' of the set 's' (expressed by `⨆ a, ↑a`). Here, `⨆` symbol is used to represent the supremum operation and `↑a` denotes the inclusion of the element 'a' in the set 's'. The statement essentially reflects the property that the supremum of a set is the largest element in that set. More concisely: For any type 'α' with a supremum operation and any set 's' of 'α', the supremum of 's' equals the supremum of its elements. In Lean notation: `sSup s = ⨆ a ∈ s, ↑a`.
`iSup_le_iff` theorem iSup_le_iff : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f : ι → α} {a : α}, iSup f ≤ a ↔ ∀ (i : ι), f i ≤ a This theorem, `iSup_le_iff`, states that for any type `α` that forms a complete lattice, any function `f` from another type `ι` to `α`, and any element `a` of `α`, the indexed supremum of `f` is less than or equal to `a` if and only if every element of `ι` when mapped by `f` is less than or equal to `a`. Here, the indexed supremum of `f` is defined as the supremum of the set of all values that `f` can take. More concisely: For any complete lattice α and function f from type ι to α, the indexed supremum of f is less than or equal to an element a of α if and only if for all i in ι, f(i) is less than or equal to a.
`iSup_apply` theorem iSup_apply : ∀ {α : Type u_9} {β : α → Type u_10} {ι : Sort u_11} [inst : (i : α) → SupSet (β i)] {f : ι → (a : α) → β a} {a : α}, (⨆ i, f i) a = ⨆ i, f i a This theorem, `iSup_apply`, states that for all types `α`, `β`, and `ι`, where `β` is dependent on `α`, along with an instance of the `SupSet` class for each `β i` where `i` is a member of `α`, and a function `f` from `ι` to `β a`, for any given `a` in `α`, the supremum, `iSup`, of `f i` evaluated at `a` is equal to the indexed supremum (denoted as ⨆ i) of `f i a`. In simpler terms, it states that the supremum of the function `f` at a particular value `a` is equivalent to the supremum of the values of `f` at `a` over all possible indices `i`. More concisely: For any type `α`, dependent type `β`, indexed family `SupSet` instances, and function `f` from `ι` to `β` indexed over `α`, the supremum of `f i` at `a` equals the indexed supremum of `f i a`.
`iInf₂_mono` theorem iInf₂_mono : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [inst : CompleteLattice α] {f g : (i : ι) → κ i → α}, (∀ (i : ι) (j : κ i), f i j ≤ g i j) → ⨅ i, ⨅ j, f i j ≤ ⨅ i, ⨅ j, g i j This theorem, `iInf₂_mono`, states that for any types `α`, `ι`, and a dependent type `κ` indexed by `ι`, given a complete lattice structure on `α`, and two functions `f` and `g` from (an `ι` and a `κ i`) to `α`, if for all `i` of type `ι` and `j` of type `κ i`, `f i j` is less than or equal to `g i j`, then the infimum of `f i j` over all `i` and `j` is less than or equal to the infimum of `g i j` over all `i` and `j`. In other words, if each element of one function is less than or equal to the corresponding element of another function, then the greatest lower bound of the first function is also less than or equal to the greatest lower bound of the second function. More concisely: If `f` and `g` are functions from `ι × κ` to a complete lattice `α` with `f(i, j) ≤ g(i, j)` for all `(i, j)`, then `⊓⁡ (λ (i, j), f i j) ≤ ⊓⁡ (λ (i, j), g i j)`. Here, `⊓⁡` denotes the infimum (greatest lower bound) operator.
`Mathlib.Order.CompleteLattice._auxLemma.7` theorem Mathlib.Order.CompleteLattice._auxLemma.7 : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f : ι → α} {a : α}, (iSup f ≤ a) = ∀ (i : ι), f i ≤ a This theorem states that for any type `α` that forms a complete lattice, any function `f` from an arbitrary type `ι` to `α`, and any element `a` of `α`, the supremum of the set of all `f(i)` (for all `i` in `ι`), denoted by `iSup f`, is less than or equal to `a` if and only if for all `i` in `ι`, `f(i)` is less than or equal to `a`. This captures the idea that the supremum of a set is the least upper bound of that set. More concisely: For any complete lattice `α`, any function `f` from a type `ι` to `α`, and any `a` in `α`, the supremum `iSup f` of `f` over `ι` is less than or equal to `a` if and only if `f(i)` is less than or equal to `a` for all `i` in `ι`.
`iSup_subtype''` theorem iSup_subtype'' : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_9} (s : Set ι) (f : ι → α), ⨆ i, f ↑i = ⨆ t ∈ s, f t := by sorry This theorem states that for any type 'α' that forms a complete lattice and for any type 'ι', given a set 's' of type 'ι' and a function 'f' mapping elements of type 'ι' to elements of type 'α', the supremum (or least upper bound) over the entire type 'ι' for 'f' applied to an element lifted from 'ι' (notated as `f ↑i`) is the same as the supremum over the set 's' for 'f' applied to an element of 's'. In other words, the least upper bound of function values over the entire type and over a set within the type are the same, for this function 'f'. More concisely: For any complete lattice 'α' and any function 'f' from a type 'ι' to 'α', the supremum of 'f' over the entire type equals the supremum of 'f' over any subset, specifically a given set 's'.
`sup_iSup_nat_succ` theorem sup_iSup_nat_succ : ∀ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α), u 0 ⊔ ⨆ i, u (i + 1) = ⨆ i, u i This theorem states that for any type `α` that is a complete lattice and a sequence `u` of elements of `α` indexed by natural numbers, the supremum (greatest lower bound) of the first element of the sequence and the supremum over the rest of the sequence is equal to the supremum over the entire sequence. In other words, the "maximum" value of the sequence doesn't change if we consider the first element separately and then take the "maximum" of the remaining sequence. More concisely: For any complete lattice `α` and sequence `u : ℕ → α`, the supremum of the first element `u 0` and the supremum of the sequence `u[1..]` equals the supremum of the entire sequence `u`.
`iSup_and` theorem iSup_and : ∀ {α : Type u_1} [inst : CompleteLattice α] {p q : Prop} {s : p ∧ q → α}, iSup s = ⨆ (h₁ : p), ⨆ (h₂ : q), s ⋯ := by sorry This theorem is about the indexed supremum of a function in the context of a complete lattice. Specifically, it states that for any type `α` forming a complete lattice, and any propositions `p` and `q`, the indexed supremum of a function `s` (which maps from the conjunction of `p` and `q` to `α`) is equal to the supremum taken over all proofs `h₁` of `p` and all proofs `h₂` of `q` of the values `s` can take. In mathematical terms, this can be written as $\sup_{(p \land q)} s = \sup_p \sup_q s$. More concisely: Given a complete lattice `α` and a function `s` from the conjunction of propositions `p` and `q` to `α`, the indexed supremum of `s` equals the supremum over all proofs `h₁` of `p` and all proofs `h₂` of `q` of the values `s h₁ h₂`. In mathematical notation, $\sup_{(p \land q)} s = \sup_p \sup_q s(h₁, h₂)$.
`sInf_lt_iff` theorem sInf_lt_iff : ∀ {α : Type u_1} [inst : CompleteLinearOrder α] {s : Set α} {b : α}, sInf s < b ↔ ∃ a ∈ s, a < b This theorem states that for any type `α` which has a `CompleteLinearOrder` structure, and for any set `s` of elements of type `α` and any element `b` of type `α`, the infimum (greatest lower bound) of the set `s` is less than `b` if and only if there exists an element `a` in the set `s` such that `a` is less than `b`. In mathematical terms, it is saying that $\inf(s) < b$ if and only if there is some $a \in s$ such that $a < b$. More concisely: For any set `s` of elements in a type `α` with a `CompleteLinearOrder` structure and any `α` element `b`, the infimum of `s` is strictly less than `b` if and only if there exists an element `a` in `s` such that `a` is strictly less than `b`.
`le_iInf₂` theorem le_iInf₂ : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ i → α}, (∀ (i : ι) (j : κ i), a ≤ f i j) → a ≤ ⨅ i, ⨅ j, f i j This theorem states that for any type `α` that forms a complete lattice, and any indexed family of functions `f : (i : ι) → κ i → α`, if `a` is less than or equal to the result of every function `f i j`, then `a` is also less than or equal to the greatest lower bound (infimum) of all values produced by these functions. In other words, if `a` is lesser or equal to all values in the set produced by the functions, then `a` is also less than or equal to the least element of that set. More concisely: If `α` is a complete lattice and `a` is less than or equal to every `f i j`, then `a` is less than or equal to the infimum of all `f i j`.
`iSup_bool_eq` theorem iSup_bool_eq : ∀ {α : Type u_1} [inst : CompleteLattice α] {f : Bool → α}, ⨆ b, f b = f true ⊔ f false := by sorry This theorem states that for any type `α` which forms a complete lattice, and for a function `f` from booleans to `α`, the supremum (or least upper bound) of `f` over all booleans equals the join (or supremum) of `f(true)` and `f(false)`. In simpler terms, when `f` is applied to all possible boolean values, the greatest value it produces is the same as the greater of the values it produces when applied to `true` and `false`. More concisely: For any complete lattice `α` and boolean-valued function `f` on `α`, the supremum of `f` over all booleans equals the join of `f(true)` and `f(false)`.
`le_iSup_iff` theorem le_iSup_iff : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteSemilatticeSup α] {a : α} {s : ι → α}, a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b This theorem states that for any type `α` that forms a complete semilattice with supremum, and any `α`-valued function `s` indexed by type `ι`, a condition `a` being less than or equal to the indexed supremum of `s` is equivalent to: for all `b` in `α`, if all elements of `s` are less than or equal to `b`, then `a` is also less than or equal to `b`. Effectively, it relates the notion of being less than or equal to the supremum of a set to the idea of being less than or equal to every upper bound of that set. More concisely: For any complete semilattice `α` with supremum and any `α`-valued function `s` indexed by type `ι`, `a ≤ sup s iff ∀b ∈ α, (∀i, s i ≤ b) → a ≤ b`.
`iInf_neg` theorem iInf_neg : ∀ {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {f : p → α}, ¬p → ⨅ (h : p), f h = ⊤ := by sorry This theorem states that for any type `α` that forms a complete lattice, for any proposition `p`, and any function `f` from `p` to `α`, if the proposition `p` is not true, then the infimum (greatest lower bound) over `f` for all `h` in the truth set of `p` is equal to the top element of the lattice (i.e., the greatest element). In other words, if the condition `p` never holds, the lower bound of the function `f` is the largest possible value in the lattice. More concisely: For any complete lattice `α` and proposition `p`, if `p` is false, then the infimum of `f` over all `h` in the truth set of `p` equals the top element of `α`.
`sSup_image'` theorem sSup_image' : ∀ {α : Type u_1} {β : Type u_2} [inst : SupSet α] {s : Set β} {f : β → α}, sSup (f '' s) = ⨆ a, f ↑a This theorem states that for any two types `α` and `β`, given a supremum-structured set `α` and a function `f` from `β` to `α`, the supremum of the image of a set `s` under the function `f`, denoted by `sSup (f '' s)`, is equal to the supremum over all elements `a` in the original set `s` of `f(a)`, denoted by `⨆ a, f ↑a`. Essentially, it's saying that the supremum of the image of a set under a function is the same as the supremum of the function values at each point in the set. This theorem is related to the concept of supremum in order theory. More concisely: For any supremum-structured set `α`, function `f` from `β` to `α`, and set `s` in `β`, the image `sSup (f '' s)` is equal to the supremum `⨆ a ∈ s, f ↑a` of the function values on `s`.
`sInf_sup_le_iInf_sup` theorem sInf_sup_le_iInf_sup : ∀ {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α}, sInf s ⊔ a ≤ ⨅ b ∈ s, b ⊔ a This theorem states that for any type `α` that is a complete lattice, and for any element `a` of this type and any set `s` of elements of this type, the supremum (least upper bound) of the set `s` join `a` is less than or equal to the infimum (greatest lower bound) over all elements `b` in the set `s` of `b` join `a`. In other words, the least upper bound of the set extended with an additional element is never greater than the greatest lower bound of all the modified sets where each element is joined with the additional element. More concisely: For any complete lattice `α` and `a` in `α`, the supremum of `a` with any subset of `α` is less than or equal to the infimum of each element in the subset joined with `a`.
`Function.Surjective.iInf_comp` theorem Function.Surjective.iInf_comp : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [inst : InfSet α] {f : ι → ι'}, Function.Surjective f → ∀ (g : ι' → α), ⨅ x, g (f x) = ⨅ y, g y The theorem `Function.Surjective.iInf_comp` states that for any type `α` with an instance of `InfSet` (which means that we can take infima of subsets of `α`), any two types `ι` and `ι'`, and any surjective function `f` from `ι` to `ι'`, the infimum of the composition of any function `g` from `ι'` to `α` with `f` over all elements in `ι` is the same as the infimum of `g` over all elements in `ι'`. In other words, if `f` is surjective, then taking infimums before or after applying `g` doesn't change the result. More concisely: For any surjective function `f` between indexed types `ι` and `ι'`, and any function `g` from `ι'` to a type `α` with an `InfSet` instance, the infimum of `g` over `ι'` is equal to the infimum of `g ∘ f` over `ι`.
`iSup_split` theorem iSup_split : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : β → α) (p : β → Prop), ⨆ i, f i = (⨆ i, ⨆ (_ : p i), f i) ⊔ ⨆ i, ⨆ (_ : ¬p i), f i This theorem states that for any type `α` that forms a complete lattice and a function `f` from another type `β` to `α`, and a given predicate `p` on `β`, the supremum of `f` over all `β` is equal to the join (supremum) of two other suprema: the supremum of `f` over all `β` that satisfy the predicate `p`, and the supremum of `f` over all `β` that do not satisfy the predicate `p`. Essentially, it's splitting the set of all `β` into two based on whether they satisfy a condition `p`, and relating the overall supremum to the suprema of these two subsets. More concisely: Given a complete lattice `α`, a function `f` from type `β` to `α`, and a predicate `p` on `β`, the supremum of `f` over `β` equals the join of the suprema of `f` over `β` satisfying `p` and those over `β` not satisfying `p`.
`le_iSup_of_le` theorem le_iSup_of_le : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f : ι → α} {a : α} (i : ι), a ≤ f i → a ≤ iSup f := by sorry This theorem states that for any type α which forms a complete lattice, an indexed function `f` from any type ι to α, and any element `a` of type α, if `a` is less than or equal to `f(i)` for some `i` in ι, then `a` is also less than or equal to the indexed supremum of `f`. In other words, any element of α that is less than or equal to the value of `f` at a particular point is also less than or equal to the supremum of the values of `f` across all of its domain. More concisely: For any complete lattice α, any indexed function f from type ι to α, and any a in α, if there exists i in ι such that a ≤ f(i), then a ≤ sup(f).
`iSup_and'` theorem iSup_and' : ∀ {α : Type u_1} [inst : CompleteLattice α] {p q : Prop} {s : p → q → α}, ⨆ (h₁ : p), ⨆ (h₂ : q), s h₁ h₂ = ⨆ (h : p ∧ q), s ⋯ ⋯ This theorem, `iSup_and'`, states that for any type `α` that forms a complete lattice, and given two propositions `p` and `q` along with a function `s` that maps a proof of `p` and a proof of `q` into `α`, the supremum (greatest lower bound) taken over all proofs of `p`, and then over all proofs of `q`, of `s` applied to these proofs, is the same as the supremum taken over all proofs of `p ∧ q` (the conjunction of `p` and `q`), of `s` applied to these proofs. This is the symmetric case of `iSup_and` and it's useful for rewriting expressions into a supremum over a conjunction. More concisely: For any complete lattice `α` and functions `s : (p: Prop) × (q: Prop) → α`, the supremum of `s(p, q)` over all proofs of `p ∧ q` is equal to the supremum of `s(p, q)` over all proofs of `p` and then over all proofs of `q`.
`iSup_prod` theorem iSup_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_4} [inst : CompleteLattice α] {f : β × γ → α}, ⨆ x, f x = ⨆ i, ⨆ j, f (i, j) This theorem, `iSup_prod`, states that for any types `α`, `β` and `γ`, with `α` being a complete lattice and `f` being a function from the product type `β × γ` to `α`, the supremum of `f` over all elements `x` of the product type is equal to the double supremum of `f` over all elements `i` of type `β` and `j` of type `γ`. In other words, the supremum of the function `f` when taken over the entire cartesian product corresponds to taking the supremum first over one component and then over the other. More concisely: For any complete lattice `α`, function `f` from the product type `β × γ` to `α`, and all `i ∈ β` and `j ∈ γ`, `⨆{x : β × γ \| f x} = ⨆{i : β} ⨆{j : γ} (f i, j)`.
`iInf_prod` theorem iInf_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_4} [inst : CompleteLattice α] {f : β × γ → α}, ⨅ x, f x = ⨅ i, ⨅ j, f (i, j) This theorem states that for any types `α`, `β` and `γ` where `α` is a complete lattice, and a function `f` from the product of `β` and `γ` to `α`, the infimum (greatest lower bound) of `f` over all pairs `(i, j)` is the same as the infimum of `f` over all `x` (where `x` is a pair from `β × γ`). In other words, it's saying that the process of finding the infimum does not change if we break the pair `(i, j)` into its individual components and find the infimum over each component separately. More concisely: For any complete lattice `α`, and a function `f` from the product `β × γ` to `α`, the infimum of `f` over all pairs `(i, j)` is equal to the infimum of `f` over all `x` in `β × γ`.
`iInf_apply` theorem iInf_apply : ∀ {α : Type u_9} {β : α → Type u_10} {ι : Sort u_11} [inst : (i : α) → InfSet (β i)] {f : ι → (a : α) → β a} {a : α}, (⨅ i, f i) a = ⨅ i, f i a This theorem states that for any indexing type `ι`, any type `α`, and a dependent type `β` based on `α`, given a function `f` from `ι` to `α` that maps each index to a value of type `β`, and some `a` of type `α`, applying the indexed infimum function `iInf` to `f` at `a` is equivalent to taking the infimum over all the values of `f i a` for each index `i`. In other words, it formalizes the concept of the infimum of a set of dependent values indexed by `ι`. More concisely: For any indexing type `ι`, type `α`, dependent type `β`, function `f` from `ι` to `α` to `β`, and `a` of type `α`, `iInf (f) a = inf { f i a \| i : ι }`.
`sInf_insert` theorem sInf_insert : ∀ {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α}, sInf (insert a s) = a ⊓ sInf s The theorem `sInf_insert` states that for any type `α` equipped with a structure of a complete lattice, any element `a` of `α`, and any set `s` of elements of `α`, the infimum (greatest lower bound) of the insertion of the element `a` into the set `s` is the infimum of the set `s` and the element `a`. This is denoted by `a ⊓ sInf s`, where `sInf` represents the infimum of a set and `⊓` is the infimum of two elements. More concisely: For any complete lattice `α`, the infimum of an element `a` and the infimum of a set `s` is equal to the infimum of the set `s` with `a` inserted. In symbols: `a ⊓ sInf s = sInf (s : set α ++ {a})`.
`CompleteSemilatticeSup.le_sSup` theorem CompleteSemilatticeSup.le_sSup : ∀ {α : Type u_9} [self : CompleteSemilatticeSup α] (s : Set α), ∀ a ∈ s, a ≤ sSup s This theorem, named `CompleteSemilatticeSup.le_sSup`, states that, for any type `α` that forms a complete semilattice with supremum (denoted as `CompleteSemilatticeSup α`) and for any set `s` of elements of type `α`, any element `a` that belongs to the set `s` is less than or equal to the supremum of the set `s`, denoted as `sSup s`. In other words, the supremum of a set in a complete semilattice is at least as great as any element in the set. More concisely: For any complete semilattice with supremum `α` and any set `s` of elements in `α`, `a ∈ s` implies `a ≤ sSup s`.
`sInf_le` theorem sInf_le : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α}, a ∈ s → sInf s ≤ a The theorem `sInf_le` states that for any type `α` that forms a complete semilattice with respect to the infimum operation, any set `s` of elements of type `α`, and any element `a` of type `α`, if `a` is an element of the set `s`, then the infimum of the set `s` is less than or equal to `a`. In other words, in a complete semilattice, the infimum of a set is always less than or equal to any element of that set. More concisely: In a complete semilattice, the infimum of any set is less than or equal to every element in the set.
`sInf_singleton` theorem sInf_singleton : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {a : α}, sInf {a} = a This theorem, `sInf_singleton`, states that for any type `α`, which is a complete semilattice under the infimum operation, the infimum (greatest lower bound) of a singleton set containing an element 'a' of type `α` is 'a' itself. In other words, if we have a set with only one element 'a', the greatest lower bound or infimum of this set is simply the element 'a'. More concisely: For any complete semilattice `α` and its element `a`, the singleton set `{a}`, if non-empty, has `a` as its infimum.
`iSup_const_le` theorem iSup_const_le : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {a : α}, ⨆ x, a ≤ a This theorem states that, for any type α that forms a complete lattice, and for any element a of this type, the supremum of any indexed set whose value is constantly a is less than or equal to a. In other words, for any set where each element is the same element a from a complete lattice, the supremum of that set will always be less than or equal to a. More concisely: For any complete lattice α and its element a, the supremum of any indexed set of elements equal to a is less than or equal to a.
`iSup_subtype'` theorem iSup_subtype' : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α}, ⨆ i, ⨆ (h : p i), f i h = ⨆ x, f ↑x ⋯ This theorem states that for any type `α` that forms a complete lattice and a predicate `p` on a sort `ι`, given a function `f` that maps an element of `ι` satisfying `p` to `α`, the supremum taken over all elements `i` and `h` such that `h` is the proof of `p i` equals the supremum taken over all `x` where `x` is of type `Subtype p` (i.e., elements of `ι` that satisfy `p`). In other words, it tells us that we can find the supremum in the lattice by either going through each element and its corresponding proof or by just considering the subtype of elements that satisfy the predicate. More concisely: Given a complete lattice `α` and a predicate `p` on a sort `ι`, the supremum of `{i \| ∃h, p i ∧ f i = x}` equals the supremum of `{x \| x ∈ Subtype p}`.
`isGLB_biInf` theorem isGLB_biInf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {s : Set β} {f : β → α}, IsGLB (f '' s) (⨅ x ∈ s, f x) The theorem `isGLB_biInf` states that for any types `α` and `β`, where `α` is a complete lattice, along with a set `s` of type `β` and a function `f` from `β` to `α`, the greatest lower bound of the image of the set `s` under the function `f` is equal to the infimum of the set of all values of `f(x)` for `x` in `s`. In other words, it asserts that the greatest lower bound of the set of all function values at elements of `s` is the infimum of these function values. More concisely: For any complete lattice α, set s of type β, and function f from β to α, the greatest lower bound of the image of s under f equals the infimum of the values in the range of f over s.
`iInf_comm` theorem iInf_comm : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [inst : CompleteLattice α] {f : ι → ι' → α}, ⨅ i, ⨅ j, f i j = ⨅ j, ⨅ i, f i j This theorem states that for any complete lattice `α` and for any two types `ι` and `ι'`, the double infimum of a function `f` taking `ι` and `ι'` to `α`, when taken first over `ι` and then over `ι'`, is equal to the double infimum taken first over `ι'` and then over `ι`. In other words, the order in which the infimums are taken does not matter. This can be interpreted as a generalization of the commutative principle to infimum operations over two different types in the context of complete lattices. More concisely: For any complete lattice `α` and functions `f: ι × ι' → α`, the double infimum `⨄⨄(f)` over `ι` then `ι'` equals the double infimum `⨄⨄(f)` over `ι'` then `ι`.
`sInf_image` theorem sInf_image : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {s : Set β} {f : β → α}, sInf (f '' s) = ⨅ a ∈ s, f a This theorem, `sInf_image`, states that for any types `α` and `β`, given `α` is a complete lattice, for any set `s` of type `β`, and any function `f` mapping elements of `β` to `α`, the infimum (the greatest lower bound) of the image of `s` under `f` (represented as `f '' s`) is equal to the infimum of `f a` for each element `a` in `s`. In mathematical terms, this theorem expresses that $\inf \{f(a) \| a \in s\} = \inf_{a \in s} f(a)$. More concisely: The infimum of the image of a set under a function equals the infimum of the function values on the set.
`iSup_dite` theorem iSup_dite : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] (p : ι → Prop) [inst_1 : DecidablePred p] (f : (i : ι) → p i → α) (g : (i : ι) → ¬p i → α), (⨆ i, if h : p i then f i h else g i h) = (⨆ i, ⨆ (h : p i), f i h) ⊔ ⨆ i, ⨆ (h : ¬p i), g i h The theorem `iSup_dite` states that for any type `α` that forms a complete lattice, any predicate `p` on some sort `ι` that is decidable, and any two functions `f` and `g` from `ι` to `α` that depend on whether `p` holds or not, respectively, the supremum (or `⨆`, the greatest lower bound in the lattice) over `ι` of the piecewise function that evaluates to `f i` if `p i` holds and `g i` otherwise, is equal to the join (`⊔`, the least upper bound in the lattice) of the supremum over `ι` of `f i` for which `p i` holds and the supremum over `ι` of `g i` for which `p i` does not hold. This theorem essentially expresses a distributive property of the supremum operation over a disjunction in a complete lattice. More concisely: For any complete lattice α, decidable predicate p on sort ι, and functions f and g from ι to α that depend on p, the supremum of the piecewise function evaluating to fi if pi holds and gi otherwise is equal to the join of the supremum of fi for pi holds and the supremum of gi for pi does not hold.
`sInf_eq_top` theorem sInf_eq_top : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, sInf s = ⊤ ↔ ∀ a ∈ s, a = ⊤ This theorem states that for any type `α` that forms a complete lattice, and any set `s` of elements of that type, the infimum of `s` (denoted `sInf s`) is equal to the top element of the lattice (denoted `⊤`) if and only if every element `a` in `s` is equal to `⊤`. In other words, in a complete lattice, a set's infimum is the top element exactly when all the set's elements are the top element. More concisely: In a complete lattice, a set's infimum is the top element if and only if every element in the set is the top element.
`iInf_top` theorem iInf_top : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α], ⨅ x, ⊤ = ⊤ This theorem, `iInf_top`, states that for any type `α` that forms a complete lattice (which is a sort of partially ordered set where any subset has a least upper bound and a greatest lower bound), the infimum (greatest lower bound) of any set `x` of elements from this lattice is always equal to the top element (`⊤`) of the lattice. This is true regardless of the specific elements in `x`, or the sorting function `ι` used. More concisely: In a complete lattice, the infimum of any set is equal to the top element.
`Monotone.map_iInf_le` theorem Monotone.map_iInf_le : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : CompleteLattice α] {s : ι → α} [inst_1 : CompleteLattice β] {f : α → β}, Monotone f → f (iInf s) ≤ ⨅ i, f (s i) The theorem `Monotone.map_iInf_le` states that for any types `α`, `β`, and `ι`, given that `α` and `β` are complete lattices, a function `f` from `α` to `β`, and `s` as a function from `ι` to `α`, if the function `f` is monotone (i.e., if `a ≤ b` then `f(a) ≤ f(b)`), then the value of `f` at the infimum (greatest lower bound) of the set `s` is less than or equal to the infimum of the set obtained by applying `f` to each element of `s`. In mathematical notation it is written as `f(inf s) ≤ inf {f(s(i)) \| i in ι}`. More concisely: If `α` and `β` are complete lattices, `f` is a monotone function from `α` to `β`, and `s` maps `ι` to `α`, then `f(∧ x in ι. s x) ≤ ∧ i in ι. f(s i)`.
`sSup_image` theorem sSup_image : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {s : Set β} {f : β → α}, sSup (f '' s) = ⨆ a ∈ s, f a This theorem states that for any types `α` and `β`, given that `α` is a complete lattice, and given a set `s` of type `β` and a function `f` from `β` to `α`, the supremum (`sSup`) of the image of `s` under `f` (`f '' s`) is equivalent to the supremum over all elements `a` in `s` of `f(a)`. In other words, the supremum of the transformed set under the function `f` is the same as the supremum over the original set with the function applied to each element. This is expressed in Lean 4 using the notation `⨆ a ∈ s, f a`. More concisely: For any complete lattice `α`, function `f` from type `β` to `α`, and set `s` of type `β`, the supremum of `f''s` equals the supremum over all `a` in `s` of `f(a)`, i.e., `sSup = ⨆ a ∈ s, f(a)`.
`sInf_eq_iInf` theorem sInf_eq_iInf : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, sInf s = ⨅ a ∈ s, a The theorem `sInf_eq_iInf` states that for any type `α` that has a complete lattice structure, and for any set `s` of elements of type `α`, the supremum of the set `s` (`sInf s`) is equal to the infimum over all elements `a` in the set `s` (`⨅ a ∈ s, a`). In other words, it asserts that the greatest lower bound of the set is the same as the least upper bound of all elements in the set, in the context of a complete lattice. More concisely: In a complete lattice, for any set, the supremum equals the infimum of its elements.
`sInf_eq_iInf'` theorem sInf_eq_iInf' : ∀ {α : Type u_1} [inst : InfSet α] (s : Set α), sInf s = ⨅ a, ↑a The theorem `sInf_eq_iInf'` states that, for any type `α` endowed with an `InfSet` structure (which allows us to take the infimum, or greatest lower bound, of a set of elements of type `α`), and for any set `s` of elements of type `α`, the supremum of the infimums (denoted by `sInf`) of the set `s` is equal to the infimum (`⨅`) of the elements of `s`, when each element is considered as a member of a larger set (indicated by `↑a`). This theorem essentially expresses a property of the interplay between suprema and infima in such structures. More concisely: For any set `s` in a type `α` endowed with an `InfSet` structure, `sInf (s : Set α) = ⨅ x ∈ s ^sup (⨅ y ∈ ↑s x)`.
`CompleteLattice.sSup_le` theorem CompleteLattice.sSup_le : ∀ {α : Type u_9} [self : CompleteLattice α] (s : Set α) (a : α), (∀ b ∈ s, b ≤ a) → sSup s ≤ a The theorem `CompleteLattice.sSup_le` states that for any type `α` which is a complete lattice, any set `s` of type `α`, and any element `a` of type `α`, if `a` is an upper bound of the set `s` (meaning every element `b` in `s` is less than or equal to `a`), then the supremum (least upper bound) of the set `s` is less than or equal to `a`. More concisely: For any complete lattice `α`, and any set `s ⊆ α` with upper bound `a` in `α`, the supremum of `s` is less than or equal to `a`.
`iSup_congr_Prop` theorem iSup_congr_Prop : ∀ {α : Type u_1} [inst : SupSet α] {p q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q), (∀ (x : q), f₁ ⋯ = f₂ x) → iSup f₁ = iSup f₂ The theorem `iSup_congr_Prop` states that for any type α with a supremum set structure, and for any propositions p and q along with functions f₁ from p to α and f₂ from q to α, if p is logically equivalent to q (denoted by `p ↔ q`), and for every instance x of q, the function f₁ applied to some value is equal to the result of function f₂ applied to x, then the indexed supremum (`iSup`) of f₁ is equal to the indexed supremum of f₂. Basically, it states that under these conditions, the supremums of the two functions with respect to their respective domains are equal. More concisely: If two propositions are logically equivalent and their corresponding functions to a type with a supremum set structure have equal values at every instance, then their indexed supremums are equal.
`iInf_union` theorem iInf_union : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {s t : Set β}, ⨅ x ∈ s ∪ t, f x = (⨅ x ∈ s, f x) ⊓ ⨅ x ∈ t, f x The theorem `iInf_union` states that for any types `α` and `β`, where `α` forms a complete lattice, and any function `f` from `β` to `α`, and any sets `s` and `t` of elements of type `β`, the infimum (greatest lower bound) of the function `f` over the union of `s` and `t` is equal to the infimum of `f` over `s` intersected with the infimum of `f` over `t`. This can be symbolized as: $\inf_{x \in s \cup t} f(x) = \inf_{x \in s} f(x) \land \inf_{x \in t} f(x)$. More concisely: The infimum of a function from a complete lattice to itself, over the union of two sets, equals the infimum over each set taken individually.
`sSup_eq_of_forall_le_of_forall_lt_exists_gt` theorem sSup_eq_of_forall_le_of_forall_lt_exists_gt : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {b : α}, (∀ a ∈ s, a ≤ b) → (∀ w < b, ∃ a ∈ s, w < a) → sSup s = b This theorem states that for any type `α` that is a complete lattice, given a set `s` of elements of type `α` and an element `b` of type `α`, if `b` is greater than or equal to all elements of `s` and for any element `w` that is less than `b`, there exists an element `a` in `s` such that `w` is less than `a`, then `b` is the supremum of the set `s`. This theorem provides an introduction rule for proving that a given element is the supremum of a set in the context of complete lattices. More concisely: If `α` is a complete lattice, `b` is an upper bound of set `s` in `α`, and for every `w` less than `b`, there exists an element `a` in `s` with `w` less than `a`, then `b` is the supremum of `s`.
`iInf_bool_eq` theorem iInf_bool_eq : ∀ {α : Type u_1} [inst : CompleteLattice α] {f : Bool → α}, ⨅ b, f b = f true ⊓ f false := by sorry This theorem states that for all types `α` that form a complete lattice, and for any function `f` from `Bool` to `α`, the infimum (greatest lower bound) over all boolean values `b` of `f(b)` is equal to the logical conjunction (AND operation) of `f(true)` and `f(false)`. Essentially, it says that the lowest value `f` can take on the boolean domain is the minimum of `f(true)` and `f(false)`. More concisely: For any complete lattice type `α` and boolean-valued function `f`: `⨧(f true, f false) = ⨋(set {bool.true, bool.false} ↔ f)` where `⨋` denotes the infimum (greatest lower bound) and `⨧` denotes the logical conjunction (AND).
`sInf_image'` theorem sInf_image' : ∀ {α : Type u_1} {β : Type u_2} [inst : InfSet α] {s : Set β} {f : β → α}, sInf (f '' s) = ⨅ a, f ↑a This theorem, named `sInf_image'`, states that for any two types `α` and `β`, where `α` has an instance of `InfSet`, and for any set `s` of type `β` and any function `f` from `β` to `α`, the infimum (`sInf`) of the image of `s` under `f` (written as `f '' s`) is equal to the infimum (`⨅ a`) over all elements `a` in the set `s` of `f` applied to `a`. Here, `↑a` is used to denote elements `a` of the set `s`, and `⨅` represents the infimum or greatest lower bound. In simpler terms, it says that the greatest lower bound of the image of a set under a function is the same as the greatest lower bound of the function values at each point in the set. More concisely: For any set `s` of type `β` with infimum `i`, and any function `f` from `β` to a type `α` with an infimum structure, the infimum of `f'' s` is equal to `i.map f`.
`iInf_subtype'` theorem iInf_subtype' : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α}, ⨅ i, ⨅ (h : p i), f i h = ⨅ x, f ↑x ⋯ This theorem states that for any complete lattice `α` and a predicate `p` on type `ι`, the infimum over `ι` of function `f` satisfying the predicate `p` is equal to the infimum of `f` over the subtype induced by the predicate `p`. In other words, the theorem ensures that the calculation of the infimum does not change when the domain of the function is restricted to a subtype defined by a certain predicate. More concisely: For any complete lattice `α` and a predicate `p` on type `ι`, the infimum of `f` over `ι` equals the infimum of `f` restricted to the subtype of `ι` where `p` holds.
`Mathlib.Order.CompleteLattice._auxLemma.10` theorem Mathlib.Order.CompleteLattice._auxLemma.10 : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {s : ι → α}, (iInf s = ⊤) = ∀ (i : ι), s i = ⊤ := by sorry The theorem `Mathlib.Order.CompleteLattice._auxLemma.10` states that for any type `α` that has a structure of a complete lattice, and any indexed set `s` with indices from `ι`, the indexed infimum (`iInf`) of `s` is equal to `⊤` (the top element of the lattice) if and only if every element of `s` is equal to `⊤`. In other words, the least upper bound (supremum) of all elements in the set is the top element of the lattice, exactly when all elements in the set are the top element of the lattice. More concisely: For any complete lattice (α, ∧, ⊧), the indexed infimum of a set s with indices from ι equals the top element ⊤ if and only if all elements in s are equal to ⊤.
`OrderIso.map_iSup` theorem OrderIso.map_iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β) (x : ι → α), f (⨆ i, x i) = ⨆ i, f (x i) The theorem `OrderIso.map_iSup` states that for any types `α` and `β` and another type `ι` (with `α` and `β` being complete lattices), and for any order isomorphism `f` from `α` to `β`, and any function `x` from `ι` to `α`, the image under `f` of the supremum (or least upper bound) over all `ι` of `x i` is equal to the supremum over all `ι` of the image under `f` of `x i`. In LaTeX notation, it's saying that for an order isomorphism `f: α -> β`, we have `f (sup_i x(i)) = sup_i f(x(i))`. More concisely: For any order isomorphism `f` between complete lattices `α` and `β`, and any function `x: ι -> α`, `f (sup_i x(i)) = sup_i f(x(i))`.
`iInf_const` theorem iInf_const : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {a : α} [inst_1 : Nonempty ι], ⨅ x, a = a This theorem states that for any type `α` that forms a complete lattice, and any value `a` of this type, the infimum of `a` over all elements `x` is just `a` itself. This holds for all nonempty types `ι`. This theorem basically says that the infimum of a constant is the constant itself, which is a standard property of infimum in lattice theory. More concisely: For any complete lattice type `α` and constant `a` in `α`, the infimum of `a` over `α` is `a` itself.
`iInf_singleton` theorem iInf_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {b : β}, ⨅ x ∈ {b}, f x = f b This theorem states that for any types `α` and `β`, given that `α` is a complete lattice, the infimum (greatest lower bound) of the set of results of a function `f` (which maps from `β` to `α`) over a singleton set containing an element `b` is equal to the result of the function `f` applied to `b`. In other words, when applied to the only element in a singleton set, the function's value is the infimum of its output over that set. More concisely: For any complete lattice `α` and function `f` from type `β` to `α`, the infimum of `{f(b) \| b : β}` is equal to `f(b)` when `β` has only one element.
`sSup_le_sSup` theorem sSup_le_sSup : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s t : Set α}, s ⊆ t → sSup s ≤ sSup t := by sorry The theorem `sSup_le_sSup` states that for all types `α` that are complete semilattices with respect to the supremum operation, and for all sets `s` and `t` of elements of type `α`, if set `s` is a subset of set `t`, then the supremum of set `s` is less than or equal to the supremum of set `t`. In other words, if all elements of a set `s` are also in a set `t`, then the least upper bound (or supremum) of `s` will not exceed the least upper bound of `t`. More concisely: For all complete semilattices with supremum operation α and sets s ⊆ t of elements in α, the supremum of s is less than or equal to the supremum of t.
`iSup_iSup_eq_left` theorem iSup_iSup_eq_left : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {b : β} {f : (x : β) → x = b → α}, ⨆ x, ⨆ (h : x = b), f x h = f b ⋯ This theorem states that for every type `α` that forms a complete lattice, a given `β` type, a specific element `b` of type `β`, and a function `f` that maps an element of type `β` and a proof that the element equals `b` to an element of type `α`, the supremum over all `β` of the supremum of `f` over the proof that `β` equals `b` is equal to the function `f` evaluated at `b`. In other words, the maximum value of `f` across all `β`s and all proofs that `β` equals `b` is just `f(b)`, assuming the supremum exists. More concisely: For every complete lattice `α`, element `b` of type `β`, and function `f` from `β × proof (β = b)` to `α`, the supremum of the supremum of `f` over all `β` and proofs that `β` equals `b` equals `f(b)`.
`CompleteLinearOrder.le_total` theorem CompleteLinearOrder.le_total : ∀ {α : Type u_9} [self : CompleteLinearOrder α] (a b : α), a ≤ b ∨ b ≤ a := by sorry This theorem states that in a complete linear order of type `α`, for any two elements `a` and `b` of that type, either `a` is less than or equal to `b` or `b` is less than or equal to `a`. A complete linear order is a mathematical structure where the relation of "less than or equal to" is defined and total, meaning that for any two elements, one must be less than or equal to the other. More concisely: In a complete linear order, any two elements are comparable, meaning that one element is less than or equal to the other.
`lt_sSup_iff` theorem lt_sSup_iff : ∀ {α : Type u_1} [inst : CompleteLinearOrder α] {s : Set α} {b : α}, b < sSup s ↔ ∃ a ∈ s, b < a The theorem `lt_sSup_iff` states that for any type `α` with a `CompleteLinearOrder` instance, any set `s` of type `α`, and any element `b` of type `α`, `b` is less than the supremum (`sSup`) of `s` if and only if there exists an element `a` in `s` such that `b` is less than `a`. This is a property of upper bounds in order theory, expressing that being less than the least upper bound of a set implies being less than some element of the set. More concisely: For any type `α` with a complete linear order and any set `s` and element `b` in `α`, `b` is strictly less than the supremum of `s` if and only if there exists an element `a` in `s` such that `b` is strictly less than `a`.
`sInf_eq_of_forall_ge_of_forall_gt_exists_lt` theorem sInf_eq_of_forall_ge_of_forall_gt_exists_lt : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {b : α}, (∀ a ∈ s, b ≤ a) → (∀ (w : α), b < w → ∃ a ∈ s, a < w) → sInf s = b This theorem, named `sInf_eq_of_forall_ge_of_forall_gt_exists_lt`, states that for all types `α` that form a complete lattice, a given set `s` of elements from this type, and a particular element `b` from this type, if `b` is less than or equal to every element in `s` and for every element `w` that is greater than `b`, there exists an element in `s` that is less than `w`, then `b` is the greatest lower bound (infimum) of the set `s`. This theorem provides an introduction rule to prove that `b` is the infimum of `s`, simply by checking two conditions: `b` is smaller than all elements of `s` and no element greater than `b` can claim the same. More concisely: If `α` is a complete lattice, `b` is in `α`, `b` is less than or equal to every element in a set `s` of `α`, and for every `w` in `α` greater than `b`, there exists an element in `s` less than `w`, then `b` is the greatest lower bound (infimum) of `s`.
`iSup_eq_dif` theorem iSup_eq_dif : ∀ {α : Type u_1} [inst : CompleteLattice α] {p : Prop} [inst_1 : Decidable p] (a : p → α), ⨆ (h : p), a h = if h : p then a h else ⊥ This theorem, `iSup_eq_dif`, asserts that for any complete lattice type `α`, any decidable proposition `p`, and any function `a` mapping from the proposition `p` to the lattice type `α`, the supremum (`⨆`) of the function `a` over all true instances `h` of the proposition `p` is equal to the value of the function `a` at `h` if `h` is true, and otherwise is equal to the bottom element (`⊥`) of the lattice `α`. In other words, it states that the supremum of a function over a decidable proposition is determined by the value of the function at the true instances of the proposition, and is the bottom element of the lattice if the proposition is false. More concisely: For any complete lattice type `α`, decidable proposition `p`, and function `a` from `p` to `α`, the supremum of `a` over true instances of `p` equals `a(h)` for `h` true in `p`, and equals the bottom element of `α` otherwise.
`iSup_of_empty` theorem iSup_of_empty : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] [inst_1 : IsEmpty ι] (f : ι → α), iSup f = ⊥ This theorem, `iSup_of_empty`, states that for any type `α` that forms a complete lattice, and for any type `ι` that is empty (i.e., there are no elements of this type), if we have a function `f` from `ι` to `α`, then the indexed supremum of `f` (`iSup f`) is equal to the bottom element (`⊥`) of the complete lattice `α`. In simpler terms, the supremum of an empty set of elements in a complete lattice is the smallest element in that lattice. More concisely: For any complete lattice `α` and empty type `ι`, the indexed supremum of the empty function from `ι` to `α` equals the bottom element of `α`.
`le_iInf_iff` theorem le_iInf_iff : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f : ι → α} {a : α}, a ≤ iInf f ↔ ∀ (i : ι), a ≤ f i This theorem states that for any type `α` that forms a complete lattice, any function `f` from an arbitrary type `ι` to `α`, and any value `a` of type `α`, the value `a` is less than or equal to the infimum of the value set produced by `f` if and only if `a` is less than or equal to the value produced by `f` for every possible input `i` of type `ι`. In other words, `a` is smaller or equal to the smallest value in the image of `f` if and only if `a` is smaller or equal to every value in the image of `f`. More concisely: For any complete lattice `α`, function `f` from type `ι` to `α`, and value `a` in `α`, `a ≤ inf (map f) a ↔ ∀ i, a ≤ (f i)`.
`sSup_insert` theorem sSup_insert : ∀ {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α}, sSup (insert a s) = a ⊔ sSup s The theorem `sSup_insert` states that for any type `α` which forms a complete lattice, and any element `a` of `α` and any set `s` of elements of `α`, the supremum of the set obtained by inserting `a` into `s` is equal to the supremum of `a` and the supremum of `s`. In other words, considering the set with an additional element, its least upper bound is the same as the least upper bound of the original set and the new element. More concisely: For any complete lattice `α`, the supremum of an element `a` in `α` and a set `s` of elements from `α` is equal to the supremum of `a` and the supremum of `s`.
`isLUB_sSup` theorem isLUB_sSup : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] (s : Set α), IsLUB s (sSup s) The theorem `isLUB_sSup` states that for any set `s` in a complete semilattice with supremum (denoted by `CompleteSemilatticeSup`), the supremum of the set `s` (denoted by `sSup s`) is a least upper bound of the set `s`. Here, a least upper bound of a set is defined as the smallest element that is greater than or equal to every element in the set. In other words, if `α` is a type that forms a complete semilattice with supremum, then for any set of elements of type `α`, the supremum of the set serves as a least upper bound for that set. More concisely: In a complete semilattice with supremum, the supremum is the least upper bound of any set.
`sSup_eq_iSup` theorem sSup_eq_iSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, sSup s = ⨆ a ∈ s, a The theorem `sSup_eq_iSup` states that for any type `α`, which is a complete lattice, and for any set `s` of elements of type `α`, the supremum (also known as the least upper bound) of the set `s` is equal to the join operation (notated by `⨆`) over all elements `a` in the set `s`. In other words, the supremum of a set in a complete lattice can be computed by taking the join of all elements in that set. More concisely: For any complete lattice α and set s ⊆ α, the supremum of s equals the join of all elements in s. (Written mathematically as ⨆s.x ≡ ⨅{x ∈ s : x ≤ y ∀y ∈ s})
`iSup_const` theorem iSup_const : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {a : α} [inst_1 : Nonempty ι], ⨆ x, a = a This theorem states that for any complete lattice `α`, any type `ι` that is nonempty, and any element `a` of `α`, the supremum of the constant function that assigns `a` to every element of `ι` is `a`. In other words, if you take any set of elements all equal to `a` from a complete lattice, the least upper bound of this set (the supremum) is also `a`. More concisely: For any complete lattice `α` and nonempty type `ι`, the supremum of the constant function mapping every element of `ι` to an arbitrary element `a` in `α` is equal to `a`.
`OrderIso.map_sSup` theorem OrderIso.map_sSup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β) (s : Set α), f (sSup s) = ⨆ a ∈ s, f a This theorem, `OrderIso.map_sSup`, states that for any types `α` and `β` that are complete lattices, and any order isomorphism `f` from `α` to `β`, and any set `s` of elements of type `α`, the image under `f` of the supremum of `s` (`sSup s`) is equal to the supremum (`⨆ a ∈ s`) of the images under `f` of the elements of `s`. In simpler terms, the order isomorphism preserves the supremum of a set. More concisely: For any complete lattices `α` and `β`, and order isomorphism `f: α ≃ β`, if `s ⊆ α` has a supremum `sSup`, then `f(sSup) = ⨆ (f x \| x ∈ s)`.
`iSup_singleton` theorem iSup_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {b : β}, ⨆ x ∈ {b}, f x = f b This theorem states that for every type `α` that is a complete lattice and for any function `f` from type `β` to `α`, the supremum (denoted with `⨆`) of `f x` over the singleton set containing only `b` is equal to `f b`. Basically, it means that the supremum of a function over a set with a single element is just the value of the function at that element. More concisely: For any complete lattice `α` and function `f` from type `β` to `α`, the supremum of `f` over a singleton set `{b}` is equal to `f b`. In mathematical notation: ⨆ {x : β \| x = b} . f x = f b.
`Prod.fst_iSup` theorem Prod.fst_iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : SupSet α] [inst_1 : SupSet β] (f : ι → α × β), (iSup f).1 = ⨆ i, (f i).1 The theorem `Prod.fst_iSup` states that for any types `α`, `β`, and index type `ι`, and for any function `f` from `ι` to a pair of elements in `α` and `β` (given that `α` and `β` are both supremum sets), the first element of the indexed supremum of `f` is equal to the supremum of the first elements of `f` over all `ι`. In other words, it is asserting that the supremum operation is preserved when applied to the first component of a sequence of pairs. More concisely: For any type `α`, index type `ι`, and function `f` from `ι` to pairs `(a, b)` in `α × β`, where `α` and `β` are supremum sets, the supremum of the first components `a` of `f` is equal to the first component of the supremum of `f`.
`iSup_bot` theorem iSup_bot : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α], ⨆ x, ⊥ = ⊥ This theorem states that for any type `α` that forms a complete lattice, and for any index type `ι`, the supremum (or least upper bound) of the bottom element `⊥` over all `x` drawn from type `ι` is equivalent to the bottom element `⊥` itself. In essence, it's asserting the property that the least upper bound of the smallest element in a complete lattice, irrespective of how we index or enumerate it, remains the smallest element. More concisely: For any complete lattice `α` and index type `ι`, the supremum of the bottom element `⊥` over all `x : ι` is equal to `⊥`.
`iSup_subtype` theorem iSup_subtype : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {p : ι → Prop} {f : Subtype p → α}, iSup f = ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ This theorem, `iSup_subtype`, states that for any type α that forms a complete lattice, a property `p` on another arbitrary type `ι`, and a function `f` mapping subtypes of `ι` that satisfy property `p` to `α`, the indexed supremum of `f` is equal to the supremum over all `i` in `ι` and all proofs `h` that `i` satisfies property `p`, of `f` applied to the subtype formed from `i` and `h`. In simpler terms, it describes a way to compute the supremum of a function applied to elements of a subtype, by instead taking the supremum over the range of the original type and the proofs that elements of this range belong to the subtype. More concisely: For any complete lattice α, property p on type ι, and function f mapping subtypes of ι satisfying p to α, the indexed supremum of f is equal to the supremum over all i in ι with property p and all proofs h that i has property p, of f applied to the subtype of i and h.
`biInf_inf` theorem biInf_inf : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α}, (∃ i, p i) → (⨅ i, ⨅ (h : p i), f i h) ⊓ a = ⨅ i, ⨅ (h : p i), f i h ⊓ a This theorem states that for any type `α` which forms a complete lattice, any indexed set of elements of `α` (via some function `f` from indices `i` of type `ι` satisfying a certain property `p` to `α`), and any element `a` of `α`, if there exists at least one index satisfying the property `p`, then the infimum over all `f i` (for `i` satisfying `p`) intersected with `a` is equal to the infimum over all `(f i) ⊓ a` (for `i` satisfying `p`). In other words, the infimum of the intersection is the same as the intersection of the infimums, provided there's some valid index. More concisely: For any complete lattice `α`, if `f : ι → α` is a function such that for some property `p` on indices `i` of type `ι`, the infimum of `{f i \| i : ι, p i}` intersect `a` equals the infimum of `{f i ⊓ a \| i : ι, p i}` when there exists an `i` satisfying `p`.
`iInf_option_elim` theorem iInf_option_elim : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (a : α) (f : β → α), ⨅ o, o.elim a f = a ⊓ ⨅ b, f b := by sorry This theorem, `iInf_option_elim`, is a version of `iInf_option` that is useful for rewriting from right to left. It states that for any types `α` and `β`, where `α` is a complete lattice, and any function `f` from `β` to `α` and element `a` of `α`, the infimum over an optional value (`o`), where `o.elim a f` is used (this means `a` is returned if `o` is `none` and `f` is applied if `o` is `some`), is equal to the meet (infimum) of `a` and the infimum over all `b` of `f b`. More concisely: For any complete lattice `α`, function `f` from type `β` to `α`, and elements `a` of `α` and `o` of type `option α`, the infimum of `a` and the infimum over all `b` in `β` of `f b` is equal to the infimum of `a` and the result of applying `o.elim` to `a` and `f`.
`iSup_ge_eq_iSup_nat_add` theorem iSup_ge_eq_iSup_nat_add : ∀ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ), ⨆ i, ⨆ (_ : i ≥ n), u i = ⨆ i, u (i + n) := by sorry This theorem states that for any type `α` that forms a complete lattice, and for any function `u` mapping natural numbers to elements of `α`, and for any natural number `n`, the supremum (greatest lower bound) of `u i` for all `i` greater than or equal to `n` is equal to the supremum of `u(i + n)` for all `i`. In other words, shifting the indices of the function by `n` doesn't change the supremum of the function values. More concisely: For any complete lattice `α` and function `u` mapping natural numbers to `α`, the supremum of `u i` for all `i ≥ n` equals the supremum of `u(i + n)` for all `i` in `ℕ`.
`iSup_range'` theorem iSup_range' : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : SupSet α] (g : β → α) (f : ι → β), ⨆ b, g ↑b = ⨆ i, g (f i) This theorem states that, for all types `α`, `β`, and `ι`, given a `SupSet` instance for `α`, and two functions `g` mapping from `β` to `α`, and `f` mapping from `ι` to `β`, the supremum of `g` applied to the elements of `β` is equal to the supremum of `g` applied to the results of applying `f` to the elements of `ι`. In other words, it doesn't matter whether we first apply `f` to `ι` and then `g` to the result, or if we directly apply `g` to `β`; the supremum remains the same. More concisely: For all types `α`, `β`, and `ι`, given a `SupSet` instance for `α`, the supremum of `g ∘ f` over `ι` equals the supremum of `g` over `β`.
`iInf_mono` theorem iInf_mono : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f g : ι → α}, (∀ (i : ι), f i ≤ g i) → iInf f ≤ iInf g The theorem `iInf_mono` states that for all types `α` and `ι`, where `α` is a complete lattice, and for all functions `f` and `g` from `ι` to `α`, if each element of `f` is less than or equal to the corresponding element of `g`, then the indexed infimum (`iInf`) of `f` is less than or equal to the indexed infimum of `g`. In other words, if all elements of one function are less than or equal to the elements of another function, then the greatest lower bound of the first function's range is less than or equal to the greatest lower bound of the second function's range. More concisely: For all complete lattices α and functions f and g from ι to α, if f i ≤ gi for all i, then iInf (f) ≤ iInf (g).
`iSup_mono` theorem iSup_mono : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f g : ι → α}, (∀ (i : ι), f i ≤ g i) → iSup f ≤ iSup g The theorem `iSup_mono` states that for any type `α` that forms a complete lattice and for any index type `ι`, given two functions `f` and `g` from `ι` to `α`, if for every `i` in `ι`, `f(i)` is less than or equal to `g(i)`, then the supremum of the range of `f` is less than or equal to the supremum of the range of `g`. Here, `iSup` is the function that calculates the supremum of the set of values obtained by applying a function to an index set. More concisely: For any complete lattice `α` and index type `ι`, if `f` and `g` are functions from `ι` to `α` with `f(i) ≤ g(i)` for all `i`, then `sup(map f) ≤ sup(map g)`.
`iSup_ne_bot_subtype` theorem iSup_ne_bot_subtype : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] (f : ι → α), ⨆ i, f ↑i = ⨆ i, f i This theorem states that for any function `f` mapping from some type `ι` to a complete lattice `α`, the supremum (the least upper bound) of `f` over all `ι` doesn't change even if we drop the elements of `ι` for which `f` returns the bottom element (`⊥`). In this context, the bottom element is the smallest element of the lattice `α`. More concisely: Given a function `f` from type `ι` to a complete lattice `α` with bottom element `⊥`, the supremum of `f` over all `ι` is equal to the supremum of `f` over the elements of `ι` that map to an element above `⊥` in `α`.
`iSup_neg` theorem iSup_neg : ∀ {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {f : p → α}, ¬p → ⨆ (h : p), f h = ⊥ := by sorry This theorem, `iSup_neg`, states that for any type `α` that forms a complete lattice, any proposition `p`, and any function `f` from `p` to `α`, if the proposition `p` is not true (denoted `¬p`), then the supremum (denoted `⨆ (h : p), f h`) of the function `f` over all `p` is the bottom element of the lattice (denoted `⊥`). Essentially, if the proposition does not hold, then the supremum of the function over the proposition equals the least element in the lattice. More concisely: If `α` is a complete lattice, `p` is a proposition over `α`, and `f` is a function from `p` to `α`, then `⨆ (h : ¬p), f h = ⊥`.
`le_sSup` theorem le_sSup : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α}, a ∈ s → a ≤ sSup s This theorem states that for any type `α` that forms a complete semilattice with a supremum and for any set `s` of elements of type `α`, any element `a` of `s` is less than or equal to the supremum of `s`. In other words, if `a` belongs to the set `s`, then `a` is always less than or equal to the least upper bound (also known as supremum) of the set `s`. More concisely: For any complete semilattice `α` with supremum and any set `s` of elements in `α`, every element `a` in `s` satisfies `a <= sup s`.
`biSup_sup` theorem biSup_sup : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α}, (∃ i, p i) → (⨆ i, ⨆ (h : p i), f i h) ⊔ a = ⨆ i, ⨆ (h : p i), f i h ⊔ a This theorem, `biSup_sup`, states that for any type `α` that forms a complete lattice, for any indexed predicate `p : ι → Prop`, for any function `f : (i : ι) → p i → α` that maps an index and a proof of that index satisfying the predicate to an element of the lattice, and for any element `a : α` of the lattice, if there exists an index for which the predicate holds, then the supremum (greatest lower bound) of the function `f` applied to all indices and proofs, joined with `a`, is equal to the supremum of the function `f` applied to all indices and proofs, each joined with `a`. In mathematical terms, it says that for a complete lattice `α`, a predicate `p` over an index set `ι`, a function `f` mapping indices and proofs of the predicate to `α`, and an element `a` in `α`, if there is some index `i` for which `p(i)` is true, then $\bigvee_i (\bigvee_{h : p(i)} f(i, h) \vee a) = \bigvee_i \bigvee_{h : p(i)} (f(i, h) \vee a)$. More concisely: For any complete lattice `α`, index set `ι`, predicate `p : ι → Prop`, function `f : (i : ι) → Prop → α`, and `a : α`, if there exists an `i` with `p(i)` such that sup(`f`(i,.)) exists, then sup(`f`(i,._) ⊎ a) = sup(∋ i, p(i) → f(i,._) ⊎ a).
`iInf_ne_top_subtype` theorem iInf_ne_top_subtype : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] (f : ι → α), ⨅ i, f ↑i = ⨅ i, f i This theorem states that when determining the infimum of a function `f : ι → α`, where α is a complete lattice, any elements of ι which `f` maps to the top element (`⊤`) can be disregarded without affecting the outcome. More formally, the infimum taken over all `i` of `f(i)` is equal to the infimum taken over all `i` of `f` applied to the coercion of `i`, and this holds for any function `f` and any type `ι`. More concisely: For any function `f : ι → α` where α is a complete lattice, the infimum of `f(i)` over all `i` is equal to the infimum of `f` applied to the coercion of `i`.
`le_iSup₂_of_le` theorem le_iSup₂_of_le : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} (i : ι) (j : κ i), a ≤ f i j → a ≤ ⨆ i, ⨆ j, f i j This theorem states that for any type `α` with a complete lattice structure, an indexed type `ι`, and a dependent type `κ` indexed by `ι`, given a function `f` that takes an index `i` from `ι` and a value `j` from the dependent type `κ i` and produces a value in `α`, if a certain value `a` in `α` is less than or equal to the result of applying `f` to `i` and `j`, then `a` is also less than or equal to the supremum (the least upper bound) over all `i` and `j` of `f` applied to `i` and `j`. This is a property related to the order structure of the complete lattice. More concisely: For any complete lattice `α` and dependent type `κ` indexed by `ι`, if `a ≤ f i j` for all `i ∈ ι` and `j ∈ κ i`, then `a ≤ sup (i, j) → f i j`.
`iInf_insert` theorem iInf_insert : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {s : Set β} {b : β}, ⨅ x ∈ insert b s, f x = f b ⊓ ⨅ x ∈ s, f x This theorem, `iInf_insert`, states that for any types `α` and `β` where `α` forms a complete lattice, for any function `f` from `β` to `α`, any set `s` of type `β`, and any element `b` of type `β`, the infimum (greatest lower bound) of the values of function `f` over the set formed by inserting `b` into `s` is equal to the infimum of the value of `f` at `b` and the infimum of the values of `f` over `s`. In other words, given a complete lattice and a function mapping elements to points in this lattice, inserting a new element into a set and taking the infimum of the function's values doesn't change the overall infimum; it's simply the meet (i.e., greatest lower bound) of the function value at the inserted element and the original infimum. More concisely: For any complete lattice `α`, function `f` from `β` to `α`, set `s ∈ β`, and `b ∈ β`, the infimum of `{f x \| x ∈ s ∪ {b}}` equals the infimum of `{f x \| x ∈ s}` and the infimum of `f b`.
`iInf_Prop_eq` theorem iInf_Prop_eq : ∀ {ι : Sort u_5} {p : ι → Prop}, ⨅ i, p i = ∀ (i : ι), p i This theorem states that for any type `ι` and for any predicate `p` that takes an instance of type `ι` and returns a proposition, the infimum (`⨅ i`) of the predicate `p` over all `i` is equivalent to the statement that the predicate `p` holds for all `i`. In other words, it says that the infimum of a set of propositions is true if and only if all propositions in the set are true. More concisely: The infimum of a set of propositions is equivalent to their conjunction.
`sup_sInf_le_iInf_sup` theorem sup_sInf_le_iInf_sup : ∀ {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α}, a ⊔ sInf s ≤ ⨅ b ∈ s, a ⊔ b This theorem states that for any type `α` that forms a complete lattice, for any element `a` of type `α`, and for any set `s` of elements of type `α`, the supremum (`⊔`) of `a` and the infimum (`sInf`) of the set `s` is less than or equal to the infimum (`⨅`) over all elements `b` in the set `s` of the supremum of `a` and `b`. In other words, the least upper bound of `a` and the greatest lower bound of the set `s` is at most the least element over all `b` in `s` that is an upper bound for both `a` and `b`. This theorem represents a weaker version of the `sup_sInf_eq` theorem in the context of complete lattices. More concisely: For any complete lattice `α`, any element `a` in `α`, and any set `s` of upper bounds for `a` in `α`, the supremum of `a` and the infimum of `s` is less than or equal to any element in `s` that is an upper bound for both `a` and all elements in `s`.
`biSup_mono` theorem biSup_mono : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f : ι → α} {p q : ι → Prop}, (∀ (i : ι), p i → q i) → ⨆ i, ⨆ (_ : p i), f i ≤ ⨆ i, ⨆ (_ : q i), f i This theorem, `biSup_mono`, states that for any type `α` which forms a complete lattice, and any function `f` from some type `ι` to `α`, along with propositions `p` and `q` about elements of type `ι`, if every element that satisfies `p` also satisfies `q`, then the supremum (greatest lower bound) of `f` over all elements that satisfy `p` is less than or equal to the supremum of `f` over all elements that satisfy `q`. This result is a demonstration of monotonicity in the context of order theory and lattice theory. More concisely: For any complete lattice `α` and function `f` from a type `ι` to `α`, if `p` implies `q` for elements of `ι`, then the supremum of `f` over elements satisfying `p` is less than or equal to the supremum over elements satisfying `q`.
`iSup_sup_eq` theorem iSup_sup_eq : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f g : ι → α}, ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ ⨆ x, g x This theorem states that for any type `α` that is a complete lattice, and any two functions `f` and `g` from type `ι` to `α`, the supremum (least upper bound) of the union of the images of `f` and `g` is equal to the union of the suprema of the images of `f` and `g`. In mathematical terms, it is expressing the property: `sup (f(x) ∪ g(x)) = sup (f(x)) ∪ sup (g(x))`. More concisely: For any complete lattice `α` and functions `f` and `g` from a type `ι` to `α`, the supremum of the union of their images equals the union of their suprema: `sup (f x ∪ g x) = sup (f x) ∪ sup (g x)`.
`sSup_le` theorem sSup_le : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α}, (∀ b ∈ s, b ≤ a) → sSup s ≤ a The theorem `sSup_le` states that for any type `α` that forms a complete semilattice with a greatest lower bound operation, any set `s` of type `α`, and any element `a` of type `α`, if every element `b` in the set `s` is less than or equal to `a`, then the supremum (greatest lower bound) of the set `s` is also less than or equal to `a`. In other words, if `a` is an upper bound for a set `s` in a complete semilattice, then the supremum of `s` cannot be greater than `a`. More concisely: If `α` is a complete semilattice with greatest lower bound operation, and `s ⊆ α` has greatest lower bound `sup s` and `a ∈ α` is an upper bound for `s`, then `sup s ≤ a`.
`IsGLB.sInf_eq` theorem IsGLB.sInf_eq : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α}, IsGLB s a → sInf s = a The theorem `IsGLB.sInf_eq` states that for any type `α` that forms a complete semilattice with an infimum operation, and for any set `s` of type `α` and an element `a` of type `α`, if `a` is a greatest lower bound of the set `s`, then the infimum of the set `s` is equal to `a`. This theorem is actually an alias of the forward direction of another theorem, `isGLB_iff_sInf_eq`. Basically, it asserts that in a complete semilattice, the infimum of a set is its greatest lower bound. More concisely: In a complete semilattice, the greatest lower bound of a set is equal to its infimum.
`iInf_le_of_le` theorem iInf_le_of_le : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f : ι → α} {a : α} (i : ι), f i ≤ a → iInf f ≤ a := by sorry The theorem `iInf_le_of_le` states that for every type `α` that is a complete lattice, and any function `f` that maps from an arbitrary type `ι` to `α`, if there exists an index `i` such that the value `f(i)` is less than or equal to a given member `a` of `α`, then the infimum (`iInf`) of the entire set range of `f` is less than or equal to `a`. In other words, if any member of the set produced by `f` is less than or equal to `a`, then the greatest lower bound (infimum) of the entire set is less than or equal to `a`. More concisely: If `f` maps an index `i` from a complete lattice `ι` to a complete lattice `α` such that `f(i) ≤ a` for some `a ∈ α`, then `iInf (range f) ≤ a`.
`iInf₂_le` theorem iInf₂_le : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [inst : CompleteLattice α] {f : (i : ι) → κ i → α} (i : ι) (j : κ i), ⨅ i, ⨅ j, f i j ≤ f i j This theorem states that for all types `α` and every function `f` from a dependent pair type `(i : ι, j : κ i)` to `α`, where `α` is a complete lattice, the infimum (or greatest lower bound) of `f` over all `i` and `j` is less than or equal to the value of `f` at any particular `(i, j)`. In other words, the value at any point in the function is always greater than or equal to the smallest value in the function. More concisely: For any complete lattice α and function f from a dependent pair type (i : ι, j : κ i) to α, the inf inf{f i j} <= f i j holds.
`Prod.fst_iInf` theorem Prod.fst_iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : InfSet α] [inst_1 : InfSet β] (f : ι → α × β), (iInf f).1 = ⨅ i, (f i).1 This theorem states that for any types `α`, `β`, and `ι`, given the infimum of any structure `InfSet` for `α` and `β`, and a function `f` from `ι` to a pair of `α` and `β`, the first component of the indexed infimum of `f` is equal to the infimum over `i` of the first component of `f i`. In terms of mathematical notation, this could be written as $(\inf f).1 = \inf_i (f(i).1)$, where `inf` represents the infimum operation, `f(i).1` selects the first component of the pair produced by `f`, and the infimum is taken over all possible values of `i`. More concisely: The first component of the infimum of a function from an index type to a pair of types is equal to the infimum of the first components of the function's applications to each index.
`iSup_inf_le_sSup_inf` theorem iSup_inf_le_sSup_inf : ∀ {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α}, ⨆ b ∈ s, b ⊓ a ≤ sSup s ⊓ a This theorem asserts that for any complete lattice `α`, any element `a` of `α`, and any set `s` of `α`, the supremum over the set `s` of the infimum of `b` and `a` (where `b` is an element of `s`) is less than or equal to the infimum of the supremum of `s` and `a`. In mathematical terms, it states that for all `α`, `a`, and `s` described above, $\sup_{b \in s} (b \land a) \leq (\sup s \land a) $. This is a weaker version of the theorem `sSup_inf_eq`. More concisely: For any complete lattice `α`, any element `a` of `α`, and any set `s` of `α`, the inf infimum of `b` and `a` for all `b` in `s` is less than or equal to the infimum of the supremum of `s` and `a`. In mathematical notation: $\inf_{b \in s} (b \land a) \leq (\inf s \land a)$.
`iSup_of_empty'` theorem iSup_of_empty' : ∀ {α : Type u_9} {ι : Sort u_10} [inst : SupSet α] [inst_1 : IsEmpty ι] (f : ι → α), iSup f = sSup ∅ This theorem, `iSup_of_empty'`, states that for any type `α` that has a supremum operation defined (indicated by `SupSet α`) and for any sort `ι` that is empty (indicated by `IsEmpty ι`), for any function `f` from `ι` to `α`, the indexed supremum of `f` (denoted by `iSup f`) is equal to the supremum of the empty set (denoted by `sSup ∅`). In simple terms, it tells us that the supremum of the image of an empty index set under any function is the same as the supremum of the empty set. More concisely: For any type `α` with a supremum operation and any empty index set `ι`, the indexed supremum of the empty function from `ι` to `α` equals the supremum of the empty set in `α`.
`iInf_le` theorem iInf_le : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] (f : ι → α) (i : ι), iInf f ≤ f i := by sorry This theorem, `iInf_le`, asserts that for any type `α` which forms a complete lattice, and any function `f` from an arbitrary type `ι` to `α`, the infimum of the range of `f` (denoted by `iInf f`) is less than or equal to the function value `f i` at any point `i` in the domain `ι`. In simpler terms, the least value in the entire range of the function `f` does not exceed the value of `f` at any specific point. More concisely: For any complete lattice `α` and function `f` from a type `ι` to `α`, the infimum of `f`'s range is less than or equal to `f(i)` for all `i` in `ι`.
`Prod.snd_iSup` theorem Prod.snd_iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : SupSet α] [inst_1 : SupSet β] (f : ι → α × β), (iSup f).2 = ⨆ i, (f i).2 The theorem `Prod.snd_iSup` states that for any types `α` and `β`, and any index type `ι`, given a function `f : ι → α × β` that maps elements of `ι` to pairs of elements from `α` and `β`, and given that `α` and `β` have supremum sets, the second component of the indexed supremum of `f` (`iSup f`).2 is equal to the supremum over `ι` of the second component of `f(i)` (`f i).2. In mathematical terms, it states that $\sup_{i} f(i)_2 = (\sup_i f(i))_2$, where $f(i)_2$ denotes the second component of the pair produced by `f`. More concisely: The second component of the indexed supremum of a function mapping elements from an index type to pairs equals the supremum of the second components of the function values over the index type.
`iSup₂_mono` theorem iSup₂_mono : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [inst : CompleteLattice α] {f g : (i : ι) → κ i → α}, (∀ (i : ι) (j : κ i), f i j ≤ g i j) → ⨆ i, ⨆ j, f i j ≤ ⨆ i, ⨆ j, g i j This theorem, `iSup₂_mono`, states that for any types `α`, `ι`, and a type function `κ` mapping from `ι`, if `α` forms a complete lattice, then for any two functions `f` and `g` from `ι` and `κ i` to `α`, if every element of `f` is less than or equal to the corresponding element in `g`, then the supremum (or least upper bound) of the set of all outputs of `f` is less than or equal to the supremum of the set of all outputs of `g`. Essentially, it says that if one function is pointwise less than or equal to another, then their suprema also obey the same inequality. More concisely: If `α` is a complete lattice and `f` and `g` are functions from `ι` to `α` with `f(i) ≤ g(i)` for all `i`, then `⨆ x. f x ≤ ⨆ x. g x`.
`sup_eq_iSup` theorem sup_eq_iSup : ∀ {α : Type u_1} [inst : CompleteLattice α] (x y : α), x ⊔ y = ⨆ b, bif b then x else y := by sorry This theorem, `sup_eq_iSup`, states that for any complete lattice `α` and any two elements `x` and `y` in `α`, the supremum (`⊔`) of `x` and `y` is equal to the indexed supremum (`⨆`) over a boolean `b`, where if `b` is true then we choose `x`, else we choose `y`. In other words, the supremum of `x` and `y` is the greatest element that is less than or equal to both `x` and `y`, and this can also be expressed as the greatest element among all elements that are either `x` or `y`, depending on the truthfulness of `b`. More concisely: For any complete lattice `α` and elements `x`, `y` in `α`, `⊔`{x, y} = `⨆`{b : Bool \| (b = true) → x ≤ y ∧ y ≤ x} or equivalently, The supremum of `x` and `y` equals the greatest element that is less than or equal to both `x` and `y`, and is also in the set {x, y}.
`Equiv.iInf_congr` theorem Equiv.iInf_congr : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [inst : InfSet α] {f : ι → α} {g : ι' → α} (e : ι ≃ ι'), (∀ (x : ι), g (e x) = f x) → ⨅ x, f x = ⨅ y, g y This theorem states that for any type `α` with an instance of InfSet, and two functions `f` and `g` from possibly different indices `ι` and `ι'` to `α`, if there exists a bijective function `e` from `ι` to `ι'` such that for all elements in `ι`, `g` applied to the image of the element under `e` gives the same result as `f` applied to the element, then the infimum over `f` for all elements in `ι` is equal to the infimum over `g` for all elements in `ι'`. In simpler terms, if the values of `f` and `g` are the same when mapped correctly, the infimum over both sets is also the same. More concisely: If `f` and `g` are functions from index sets `ι` and `ι'` to a type `α` with an instance of InfSet, and there exists a bijective function `e` from `ι` to `ι'` such that `g ∘ e = f` pointwise, then `inf (map f ι) = inf (map g ι')`.
`OrderIso.map_sInf` theorem OrderIso.map_sInf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β) (s : Set α), f (sInf s) = ⨅ a ∈ s, f a The theorem `OrderIso.map_sInf` states that for any two types `α` and `β` equipped with a complete lattice structure, and given an order isomorphism `f` from `α` to `β` and a set of elements `s` from `α`, the image under `f` of the infimum (or greatest lower bound) of `s` in `α` is equal to the infimum of the image of `s` under `f` in `β`. In other words, the order isomorphism `f` preserves the operation of taking infima. More concisely: For order isomorphisms between complete lattices, the image of the infimum of a set under the isomorphism is equal to the infimum of the image of that set.
`Mathlib.Order.CompleteLattice._auxLemma.8` theorem Mathlib.Order.CompleteLattice._auxLemma.8 : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f : ι → α} {a : α}, (a ≤ iInf f) = ∀ (i : ι), a ≤ f i The theorem `Mathlib.Order.CompleteLattice._auxLemma.8` states that for any type `α` that is a complete lattice, any function `f` from some index type `ι` to `α`, and any element `a` of `α`, the condition that `a` is less than or equal to the indexed infimum of `f` (denoted as `iInf f`) is equivalent to the condition that `a` is less than or equal to `f i` for all `i` in `ι`. In other words, an element is less than or equal to the infimum of the function's range if and only if it is less than or equal to all elements in the function's range. More concisely: For any complete lattice α and function f from an index type ι to α, an element a of α is less than or equal to the infimum of f if and only if it is less than or equal to f(i) for all i in ι.
`iSup₂_le` theorem iSup₂_le : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ i → α}, (∀ (i : ι) (j : κ i), f i j ≤ a) → ⨆ i, ⨆ j, f i j ≤ a This theorem states that, for any type `α` that forms a complete lattice, any element `a` of `α`, and any function `f` mapping elements of type `ι` and `κ i` to `α`, if for all `i` and `j`, `f(i, j)` is less than or equal to `a`, then the supremum over all `i` and `j` of `f(i, j)` is also less than or equal to `a`. In mathematical terms, if each element in a set is less than or equal to `a`, then the least upper bound (supremum) of the set is also less than or equal to `a`. More concisely: For any complete lattice `α`, any element `a` in `α`, and any function `f` from a set into `α`, if `f(i) ≤ a` for all `i`, then `⨆ i. f(i) ≤ a`. (Here, `⨆` denotes the supremum or least upper bound over the index set `i`.)
`iInf₂_le_of_le` theorem iInf₂_le_of_le : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_7} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ i → α} (i : ι) (j : κ i), f i j ≤ a → ⨅ i, ⨅ j, f i j ≤ a This theorem states that for all types `α` and `ι`, and for all functions `κ` from `ι` to a sorted type, given `α` is a complete lattice, and given `a` of type `α` and a function `f` mapping each `ι` and `κ i` to `α`, for any `i` of type `ι` and `j` of type `κ i`, if `f i j` is less than or equal to `a`, then the infimum (`⨅`) over all `i` and for each `i`, `j` (i.e., the greatest lower bound) of `f i j` is less than or equal to `a`. In other words, if a particular value from a double-indexed set is less than or equal to `a`, then the greatest lower bound of the entire set is also less than or equal to `a`. More concisely: For any complete lattice `α`, function `κ` from a type `ι` to `α`, `a` in `α`, and function `f` mapping each pair `(i, j)` in `ι × κ` to `α` such that `f i j ≤ a` for all `i` and `j`, the infimum of `f i j` over all `i` and `j` is less than or equal to `a`.
`iSup_inf_le_inf_sSup` theorem iSup_inf_le_inf_sSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α}, ⨆ b ∈ s, a ⊓ b ≤ a ⊓ sSup s This theorem states that for any type `α` which has a complete lattice structure, for any element `a` of `α` and any subset `s` of `α`, the supremum (i.e., least upper bound) of the set of all infimum (i.e., greatest lower bound) of `a` and elements `b` in `s` is less than or equal to the infimum of `a` and the supremum of `s`. This is a weaker version of the theorem `inf_sSup_eq`. More concisely: For any complete lattice `α` and its elements `a` and any subset `s` of `α`, the infimum of `a` and the supremum of the set of infima of `a` and elements in `s` is less than or equal to the infimum of `a` and the supremum of `s`.
`iInf_of_empty` theorem iInf_of_empty : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] [inst_1 : IsEmpty ι] (f : ι → α), iInf f = ⊤ The theorem `iInf_of_empty` states that for any type `α` forming a complete lattice, and for any function `f` mapping from an empty type `ι` to `α`, the indexed infimum (`iInf`) of `f` is the top element (`⊤`) of the lattice. In other words, when the domain of a function is an empty set, the infimum over the range of that function in a complete lattice is the greatest element in the lattice. More concisely: For any complete lattice `α` and empty type `ι`, the indexed infimum of the empty function from `ι` to `α` is the top element of `α`.
`iInf_of_isEmpty` theorem iInf_of_isEmpty : ∀ {α : Type u_9} {ι : Sort u_10} [inst : InfSet α] [inst_1 : IsEmpty ι] (f : ι → α), iInf f = sInf ∅ The theorem `iInf_of_isEmpty` states that for any type `α` with an infimum on sets (`InfSet α`) and any type `ι` that is empty (`IsEmpty ι`), for any function `f` from `ι` to `α`, the indexed infimum of `f` (`iInf f`) is equal to the supremum of an empty set (`sInf ∅`). In other words, if we are taking the infimum over an indexed family, and that index set is empty, then the result is the same as taking the infimum of the empty set. More concisely: For any type `α` with an infimum on sets, any empty type `ι`, and any function `f` from `ι` to `α`, the indexed infimum `iInf f` is equal to the supremum of the empty set `sInf ∅`.
`iInf_subtype''` theorem iInf_subtype'' : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_9} (s : Set ι) (f : ι → α), ⨅ i, f ↑i = ⨅ t ∈ s, f t := by sorry This theorem states that for any complete lattice `α` of some type `u_1`, and for any set `s` of type `ι`, the function `f` mapping elements of `ι` to `α`, the infimum (greatest lower bound) over all `i` of `f` applied to the elements of `ι` in the set `s` is equal to the infimum over all elements `t` in the set `s` of `f` applied to `t`. In other words, it asserts the equality of two different ways of calculating the infimum of a function applied to the elements of a set, one using the direct elements and the other using their subtype representation. More concisely: For any complete lattice `α` and set `s` of index type `ι`, the infimum of a function `f` from `ι` to `α` over `s` equals the infimum of the images of elements in `s` under `f`.
`isLUB_iSup` theorem isLUB_iSup : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f : ι → α}, IsLUB (Set.range f) (⨆ j, f j) This theorem, `isLUB_iSup`, states that for any type `α` that forms a complete lattice and for any function `f` from some type `ι` to `α`, the least upper bound (LUB) of the range of `f` is the supremum of the function `f` over all `j` in `ι`. In other words, the least upper bound of the set of all possible outputs of `f` is exactly the supremum of the outputs of `f`. More concisely: For any complete lattice `α` and function `f` from a type `ι` to `α`, the LUB of `f`'s range equals the supremum of `f` over all elements in `ι`.
`isGLB_iInf` theorem isGLB_iInf : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f : ι → α}, IsGLB (Set.range f) (⨅ j, f j) The theorem `isGLB_iInf` states that for any type `α` which is a complete lattice, and any function `f` from some type `ι` to `α`, the greatest lower bound (GLB) of the range of `f` is equal to the infimum of the set of all `f j` as `j` varies over the type `ι`. In other words, the smallest element that is greater than or equal to every element in the range of `f` is the same as the least element of the set of all `f j`. This property holds in the setting of complete lattices, which are partially ordered sets in which every subset has both a greatest lower bound and a least upper bound. More concisely: In a complete lattice, the greatest lower bound of the range of a function equals the infimum of its values.
`Monotone.le_map_iSup₂` theorem Monotone.le_map_iSup₂ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_7} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {f : α → β}, Monotone f → ∀ (s : (i : ι) → κ i → α), ⨆ i, ⨆ j, f (s i j) ≤ f (⨆ i, ⨆ j, s i j) The theorem `Monotone.le_map_iSup₂` states that for any two types `α` and `β`, where both `α` and `β` are complete lattices, any function `f` from `α` to `β`, and any family of sets `s` indexed by two sorts `ι` and `κ`, if the function `f` is monotone, then the supremum (denoted by ⨆) of the function `f` applied to the elements of the sets in the family `s` is less than or equal to the function `f` applied to the supremum of the elements of the sets in the family `s`. In other words, the function `f` preserves the order of the suprema. More concisely: For any complete lattices α and β, monotone function f : α → β, and families s : ι → Set κ with supremum s.sup, f (⨆ x in s : α) ≤ ⨆ x in s : α → β. (f(x))
`iInf_le_iInf_of_subset` theorem iInf_le_iInf_of_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {s t : Set β}, s ⊆ t → ⨅ x ∈ t, f x ≤ ⨅ x ∈ s, f x This theorem states that for any two types `α` and `β`, where `α` is a complete lattice, and for any function `f` from `β` to `α` and any two sets `s` and `t` of type `β`, if `s` is a subset of `t`, then the infimum (greatest lower bound) of the image of `t` under `f` is less than or equal to the infimum of the image of `s` under `f`. In other words, if we apply `f` to each element of `t` and `s` and take the greatest lower bound of the results, the value for `t` will be less than or equal to the value for `s`. More concisely: For any complete lattice `α`, function `f` from type `β` to `α`, and sets `s` and `t` of type `β` with `s` a subset of `t`, the infimum of `f``[t]` is less than or equal to the infimum of `f``[s]`. Here, `f``[X]` denotes the image of set `X` under function `f`.
`lt_iSup_iff` theorem lt_iSup_iff : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLinearOrder α] {a : α} {f : ι → α}, a < iSup f ↔ ∃ i, a < f i := by sorry The theorem `lt_iSup_iff` states that for any type `α` that has a complete linear order, a value `a` of type `α`, and a function `f` from some type `ι` to `α`, `a` is less than the indexed supremum of `f` if and only if there exists an element `i` of type `ι` such that `a` is less than `f(i)`. In mathematical terms, this is saying that $a$ is less than the supremum of the range of $f$ if and only if there exists an $i$ in the domain of $f$ such that $a$ is less than $f(i)$. More concisely: For any complete linear order `α`, element `a` of `α`, and function `f` from some type `ι` to `α`, `a` is less than the indexed supremum of `f` if and only if there exists an `i` in `ι` such that `a` is less than `f(i)`. Or mathematically, $a < \sup\_{i\in \mathrm{dom}(f)} f(i)$.
`Monotone.le_map_iSup` theorem Monotone.le_map_iSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : CompleteLattice α] {s : ι → α} [inst_1 : CompleteLattice β] {f : α → β}, Monotone f → ⨆ i, f (s i) ≤ f (iSup s) This theorem states that for any complete lattices `α` and `β`, any mapping `s` from some sort `ι` to `α`, and any function `f` from `α` to `β`, if `f` is monotone (that is, `f` preserves the ordering, i.e., if `a ≤ b`, then `f(a) ≤ f(b)`), then the supremum (indexed by `ι`) of the function `f` applied to `s` is less than or equal to the function `f` applied to the supremum of `s`. In other words, the supremum of the image under `f` is less than or equal to the image of the supremum under `f` as long as `f` is a monotone function. More concisely: For any complete lattices α and β, any map s from sort ι to α, and monotone function f from α to β, the supremum of f(s) is less than or equal to f(sup s).
`OrderIso.map_sInf_eq_sInf_symm_preimage` theorem OrderIso.map_sInf_eq_sInf_symm_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β) (s : Set α), f (sInf s) = sInf (⇑f.symm ⁻¹' s) The theorem `OrderIso.map_sInf_eq_sInf_symm_preimage` states that for any two types `α` and `β` that are complete lattices and an order isomorphism `f` from `α` to `β`, the smallest element (`sInf`) of a set `s` of type `α` mapped through `f` is equal to the smallest element of the preimage of `s` under the inverse (`OrderIso.symm f`) of `f`. In other words, applying the order isomorphism to the smallest element of a set in `α` gives the same result as finding the smallest element of the corresponding set in `β`. More concisely: Given complete lattices α and β and an order isomorphism f : α ↔ β, the smallest element of the image of a subset s of α under f is equal to the smallest element of the preimage of s under the inverse of f.
`iInf_congr_Prop` theorem iInf_congr_Prop : ∀ {α : Type u_1} [inst : InfSet α] {p q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q), (∀ (x : q), f₁ ⋯ = f₂ x) → iInf f₁ = iInf f₂ This theorem states that for any type `α` that has an infimum and any propositions `p` and `q`, if there exist functions `f₁ : p → α` and `f₂ : q → α`, then the indexed infimum of `f₁` is equal to the indexed infimum of `f₂` if and only if two conditions are met: (1) `p` and `q` are logically equivalent (i.e., `p` if and only if `q`), and (2) for all `x` in the domain of `f₂`, the output of `f₁` applied to some value corresponding to `x` (under the logical equivalence) is equal to `f₂ x`. Essentially, this theorem guarantees that the indexed infimum is preserved under changes that maintain logical equivalence and function output equivalence. More concisely: For types `α` with an infimum and propositions `p` and `q`, if there exist functions `f₁ : p → α` and `f₂ : q → α` such that `p` is logically equivalent to `q` and `f₁(x) = f₂(y)` for all `x` in the domain of `f₂` and corresponding `y` under the logical equivalence, then the indexed infima of `f₁` and `f₂` are equal.
`iSup_sup` theorem iSup_sup : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] [inst_1 : Nonempty ι] {f : ι → α} {a : α}, (⨆ x, f x) ⊔ a = ⨆ x, f x ⊔ a This theorem states that for any type `α` which forms a complete lattice, any nonempty type `ι`, a function `f` from `ι` to `α`, and an element `a` of `α`, the supremum of `f x` for all `x` in `ι` joined with `a` is equal to the supremum of the joined elements `f x` and `a` for all `x` in `ι`. In more mathematical terms, it says that for any function `f: ι → α` and any `a ∈ α`, we have `sup_x (f(x)) ∨ a = sup_x (f(x) ∨ a)`. This is a property of complete lattices and the sup operation. More concisely: For any complete lattice `α`, any nonempty type `ι`, and function `f` from `ι` to `α`, the supremum of `f x` for all `x` in `ι` joined with an element `a` of `α` is equal to the supremum of the joined elements `f x` and `a` for all `x` in `ι`. In symbols, `sup_x (f(x) ∨ a) = sup_x (f(x)) ∨ a`.
`iSup_Prop_eq` theorem iSup_Prop_eq : ∀ {ι : Sort u_5} {p : ι → Prop}, ⨆ i, p i = ∃ i, p i This theorem states that for any indexed type `ι` and any proposition function `p` from `ι` to `Prop`, the supremum over `i` of `p i` is equal to the existence of an `i` for which `p i` holds. In other words, the supremum of the proposition `p` over all `i` is true if and only if there exists some `i` for which `p i` is true. More concisely: The supremum of an indexed proposition `p : ι → Prop` equals the existence of an element `i` in `ι` such that `p i` holds.
`iSup_option_elim` theorem iSup_option_elim : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (a : α) (f : β → α), ⨆ o, o.elim a f = a ⊔ ⨆ b, f b := by sorry This theorem, `iSup_option_elim`, is a variant of `iSup_option` that is useful for rewriting from right to left. Given an arbitrary complete lattice `α`, an element `a` of `α`, and a function `f` from another arbitrary type `β` to `α`, the theorem states that the supremum (greatest lower bound) over the option type of the function `o.elim a f`, is equal to the join of `a` and the supremum over `β` of `f b`. In simpler terms, this theorem relates the supremum of the function over all possible values including the option of no value (represented by `a`) to the supremum of the function over all definite values. More concisely: The supremum of the option elimination of a function `f` over an option type is equal to the join of the element `a` and the supremum of `f` over its domain.

LeanAide GPT-4 documentation

Module: Mathlib.Order.CompleteLattice

iInf_true

theorem iInf_true : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : True → α}, iInf s = s trivial

iInf_subtype

theorem iInf_subtype : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {p : ι → Prop} {f : Subtype p → α}, iInf f = ⨅ i, ⨅ (h : p i), f ⟨i, h⟩

iSup_univ

theorem iSup_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α}, ⨆ x ∈ Set.univ, f x = ⨆ x, f x

CompleteLattice.le_sInf

theorem CompleteLattice.le_sInf : ∀ {α : Type u_9} [self : CompleteLattice α] (s : Set α) (a : α), (∀ b ∈ s, a ≤ b) → a ≤ sInf s

CompleteLattice.le_top

theorem CompleteLattice.le_top : ∀ {α : Type u_9} [self : CompleteLattice α] (x : α), x ≤ ⊤

Monotone.iSup_nat_add

theorem Monotone.iSup_nat_add : ∀ {α : Type u_1} [inst : CompleteLattice α] {f : ℕ → α}, Monotone f → ∀ (k : ℕ), ⨆ n, f (n + k) = ⨆ n, f n := by sorry

le_sInf_iff

theorem le_sInf_iff : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α}, a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b

iInf_mono'

theorem iInf_mono' : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [inst : CompleteLattice α] {f : ι → α} {g : ι' → α}, (∀ (i' : ι'), ∃ i, f i ≤ g i') → iInf f ≤ iInf g

iSup_comp_le

theorem iSup_comp_le : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {ι' : Sort u_9} (f : ι' → α) (g : ι → ι'), ⨆ x, f (g x) ≤ ⨆ y, f y

iSup_comm

theorem iSup_comm : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [inst : CompleteLattice α] {f : ι → ι' → α}, ⨆ i, ⨆ j, f i j = ⨆ j, ⨆ i, f i j

iInf_range

theorem iInf_range : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : CompleteLattice α] {g : β → α} {f : ι → β}, ⨅ b ∈ Set.range f, g b = ⨅ i, g (f i)

IsLUB.sSup_eq

theorem IsLUB.sSup_eq : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α}, IsLUB s a → sSup s = a

sSup_range

theorem sSup_range : ∀ {α : Type u_1} {ι : Sort u_5} [inst : SupSet α] {f : ι → α}, sSup (Set.range f) = iSup f := by sorry

iSup_option

theorem iSup_option : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : Option β → α), ⨆ o, f o = f none ⊔ ⨆ b, f (some b)

iSup_pos

theorem iSup_pos : ∀ {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {f : p → α} (hp : p), ⨆ (h : p), f h = f hp

sInf_le_sInf

theorem sInf_le_sInf : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s t : Set α}, s ⊆ t → sInf t ≤ sInf s := by sorry

CompleteLattice.le_sSup

theorem CompleteLattice.le_sSup : ∀ {α : Type u_9} [self : CompleteLattice α] (s : Set α), ∀ a ∈ s, a ≤ sSup s := by sorry

sSup_singleton

theorem sSup_singleton : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {a : α}, sSup {a} = a

iInf_inf_eq

theorem iInf_inf_eq : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f g : ι → α}, ⨅ x, f x ⊓ g x = (⨅ x, f x) ⊓ ⨅ x, g x

iSup_insert

theorem iSup_insert : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {s : Set β} {b : β}, ⨆ x ∈ insert b s, f x = f b ⊔ ⨆ x ∈ s, f x

CompleteSemilatticeInf.sInf_le

theorem CompleteSemilatticeInf.sInf_le : ∀ {α : Type u_9} [self : CompleteSemilatticeInf α] (s : Set α), ∀ a ∈ s, sInf s ≤ a

CompleteSemilatticeSup.sSup_le

theorem CompleteSemilatticeSup.sSup_le : ∀ {α : Type u_9} [self : CompleteSemilatticeSup α] (s : Set α) (a : α), (∀ b ∈ s, b ≤ a) → sSup s ≤ a

iInf_congr

theorem iInf_congr : ∀ {α : Type u_1} {ι : Sort u_5} [inst : InfSet α] {f g : ι → α}, (∀ (i : ι), f i = g i) → ⨅ i, f i = ⨅ i, g i := by sorry

iSup_le_iSup_of_subset

theorem iSup_le_iSup_of_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {s t : Set β}, s ⊆ t → ⨆ x ∈ s, f x ≤ ⨆ x ∈ t, f x

sSup_apply

theorem sSup_apply : ∀ {α : Type u_9} {β : α → Type u_10} [inst : (i : α) → SupSet (β i)] {s : Set ((a : α) → β a)} {a : α}, sSup s a = ⨆ f, ↑f a

iSup_exists

theorem iSup_exists : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {p : ι → Prop} {f : Exists p → α}, ⨆ (x : Exists p), f x = ⨆ i, ⨆ (h : p i), f ⋯

Prod.snd_iInf

theorem Prod.snd_iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : InfSet α] [inst_1 : InfSet β] (f : ι → α × β), (iInf f).2 = ⨅ i, (f i).2

isGLB_sInf

theorem isGLB_sInf : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] (s : Set α), IsGLB s (sInf s)

OrderIso.map_iInf

theorem OrderIso.map_iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β) (x : ι → α), f (⨅ i, x i) = ⨅ i, f (x i)

iSup_congr

theorem iSup_congr : ∀ {α : Type u_1} {ι : Sort u_5} [inst : SupSet α] {f g : ι → α}, (∀ (i : ι), f i = g i) → ⨆ i, f i = ⨆ i, g i := by sorry

iSup_eq_top

theorem iSup_eq_top : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLinearOrder α] (f : ι → α), iSup f = ⊤ ↔ ∀ b < ⊤, ∃ i, b < f i := by sorry

iSup_eq_bot

theorem iSup_eq_bot : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {s : ι → α}, iSup s = ⊥ ↔ ∀ (i : ι), s i = ⊥

iSup_sigma

theorem iSup_sigma : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {p : β → Type u_9} {f : Sigma p → α}, ⨆ x, f x = ⨆ i, ⨆ j, f ⟨i, j⟩

CompleteLattice.bot_le

theorem CompleteLattice.bot_le : ∀ {α : Type u_9} [self : CompleteLattice α] (x : α), ⊥ ≤ x

sSup_le_iff

theorem sSup_le_iff : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α}, sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a

le_iInf

theorem le_iInf : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f : ι → α} {a : α}, (∀ (i : ι), a ≤ f i) → a ≤ iInf f

iSup_range

theorem iSup_range : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : CompleteLattice α] {g : β → α} {f : ι → β}, ⨆ b ∈ Set.range f, g b = ⨆ i, g (f i)

iSup_mono'

theorem iSup_mono' : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} [inst : CompleteLattice α] {f : ι → α} {g : ι' → α}, (∀ (i : ι), ∃ i', f i ≤ g i') → iSup f ≤ iSup g

iInf_emptyset

theorem iInf_emptyset : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α}, ⨅ x ∈ ∅, f x = ⊤ := by sorry

`iInf_true`

`iInf_subtype`

`iSup_univ`

`CompleteLattice.le_sInf`

`CompleteLattice.le_top`

`Monotone.iSup_nat_add`

`le_sInf_iff`

`iInf_mono'`

`iSup_comp_le`

`iSup_comm`

`iInf_range`

`IsLUB.sSup_eq`

`sSup_range`

`iSup_option`

`iSup_pos`

`sInf_le_sInf`

`CompleteLattice.le_sSup`

`sSup_singleton`

`iInf_inf_eq`

`iSup_insert`

`CompleteSemilatticeInf.sInf_le`

`CompleteSemilatticeSup.sSup_le`

`iInf_congr`

`iSup_le_iSup_of_subset`

`sSup_apply`

`iSup_exists`

`Prod.snd_iInf`

`isGLB_sInf`

`OrderIso.map_iInf`

`iSup_congr`

`iSup_eq_top`

`iSup_eq_bot`

`iSup_sigma`

`CompleteLattice.bot_le`

`sSup_le_iff`

`le_iInf`

`iSup_range`

`iSup_mono'`

`iInf_emptyset`

`le_iSup₂`

`iSup_const_mono`

`inf_eq_iInf`

`Function.Surjective.iSup_congr`

`iInf_image`

`iSup_eq_of_forall_le_of_forall_lt_exists_gt`

`iSup_iSup_eq_right`

`iInf_pos`

`iSup_or`

`biInf_mono`

`le_sInf`

`iSup_image`

`Function.Surjective.iInf_congr`

`CompleteLattice.sInf_le`

`iSup_union`

`le_iSup`

`Function.Surjective.iSup_comp`

`iInf_eq_of_forall_ge_of_forall_gt_exists_lt`

`iInf_and`

`iInf_iInf_eq_left`

`iSup_le`

`CompleteSemilatticeInf.le_sInf`

`sInf_empty`

`sSup_eq_bot`

`le_iSup_inf_iSup`

`sInf_range`

`sSup_empty`

`sSup_pair`

`iSup_plift_down`

`OrderIso.map_sSup_eq_sSup_symm_preimage`

`iInf_and'`

`biSup_prod`

`sSup_eq_iSup'`

`iSup_le_iff`

`iSup_apply`