le_csInf
theorem le_csInf :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α},
s.Nonempty → (∀ b ∈ s, a ≤ b) → a ≤ sInf s
The theorem `le_csInf` states that for any type `α` that is a conditionally complete lattice, and any set `s` of type `α`, and any element `a` of type `α`, if the set `s` is not empty, and all elements `b` in `s` satisfy the property that `a` is less than or equal to `b`, then `a` is less than or equal to the infimum of the set `s`.
In other words, this theorem states that if we have a non-empty set within a conditionally complete lattice, and some element is less than or equal to all elements of this set, then this element is also less than or equal to the greatest lower bound (infimum) of this set.
More concisely: If `α` is a conditionally complete lattice, `s ≠ ∅` is a set of `α`, and `a ≤ b` for all `b ∈ s`, then `a ≤ ∧ b ∈ s`.
|
ciSup_mono
theorem ciSup_mono :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {f g : ι → α},
BddAbove (Set.range g) → (∀ (x : ι), f x ≤ g x) → iSup f ≤ iSup g
This theorem, named `ciSup_mono`, states that for any type `α` with a conditionally complete lattice structure, and any sort `ι`, if you have two functions `f` and `g` from `ι` to `α`, then the supremum of `f` is less than or equal to the supremum of `g` provided that two conditions are satisfied: (1) the set of all values that `g` can take (i.e., the range of `g`) is bounded above, and (2) for every element `x` of type `ι`, the value of `f` at `x` is less than or equal to the value of `g` at `x`. In mathematical terms, if `g` is bounded above and `f(x) ≤ g(x)` for all `x`, then `sup(f) ≤ sup(g)`.
More concisely: If `α` is a type with a conditionally complete lattice structure, and `f` and `g` are functions from a bounded-above set `ι` to `α` with `f(x) ≤ g(x)` for all `x ∈ ι`, then `sup(f) ≤ sup(g)`.
|
IsGLB.csInf_eq
theorem IsGLB.csInf_eq :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α}, IsGLB s a → s.Nonempty → sInf s = a
This theorem states that for any type `α` that is a `ConditionallyCompleteLattice`, for any set `s` of `α`, and for any element `a` of `α`, if `a` is the greatest lower bound of `s` and `s` is not empty, then the infimum (`sInf`) of `s` is equal to `a`. Here, a `ConditionallyCompleteLattice` is a type that is a lattice with a least element and greatest element, and `sInf` is the greatest element less than or equal to all elements in the set.
More concisely: For any non-empty set `s` of a `ConditionallyCompleteLattice` type `α` and any element `a` that is the greatest lower bound of `s`, we have `a = s.inf`.
|
ciSup_le
theorem ciSup_le :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] [inst_1 : Nonempty ι] {f : ι → α} {c : α},
(∀ (x : ι), f x ≤ c) → iSup f ≤ c
This theorem states that for any type `α` that is a conditionally complete lattice and any nonempty type `ι`, given a function `f` from `ι` to `α` and any element `c` of `α`, if all values of the function `f` are less than or equal to `c`, then the indexed supremum (or least upper bound) of the function `f`, denoted `iSup f`, is also less than or equal to `c`. In simple terms, if every output of a function is bounded by a certain value, then the supremum of these outputs cannot exceed this bound.
More concisely: If `α` is a conditionally complete lattice and `f : ι → α` is a function with domain `ι` such that `∀ i, f i ≤ c`, then `iSup f ≤ c`.
|
le_ciInf
theorem le_ciInf :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] [inst_1 : Nonempty ι] {f : ι → α} {c : α},
(∀ (x : ι), c ≤ f x) → c ≤ iInf f
The theorem `le_ciInf` states that for any type `α` that forms a conditionally complete lattice and any nonempty indexing type `ι`, given a function `f` from `ι` to `α` and an element `c` of `α`, if `c` is less than or equal to the value of `f` at every point in the indexing type `ι`, then `c` is less than or equal to the indexed infimum of `f`. In other words, if `c` is a lower bound for the range of `f`, then `c` is less than or equal to the greatest lower bound of the range of `f`.
More concisely: If `α` is a conditionally complete lattice and `f: ι → α` is a function with `c ∈ α` being a lower bound of `{f x | x ∈ ι}`, then `c ≤ ⨯₋ x. (f x)` (infimum of `f`).
|
WithTop.iInf_coe_eq_top
theorem WithTop.iInf_coe_eq_top :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] {f : ι → α},
⨅ x, ↑(f x) = ⊤ ↔ IsEmpty ι
This theorem states that for any type `α` with the property of `ConditionallyCompleteLinearOrderBot` (a kind of order structure) and any function `f` from some type `ι` to `α`, the infimum (greatest lower bound) of the co-domain of `f`, when considered in the extended real number line with a top element, is equal to `⊤`(top) if and only if `ι` is an empty type. In other words, if we have no inputs (i.e., `ι` is empty), then the infimum of the image of `f` is the top element.
More concisely: For any function `f` from an empty type to a type `α` with the property `ConditionallyCompleteLinearOrderBot`, the infimum of the image of `f` in the extended real numbers is the top element.
|
le_csInf_iff''
theorem le_csInf_iff'' :
∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α},
s.Nonempty → (a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b)
This theorem, `le_csInf_iff''`, states that for any type `α` equipped with a conditionally complete linear order structure and a lowest element (`ConditionallyCompleteLinearOrderBot α`), for any set `s` of type `α`, and for any element `a` of type `α`, if the set `s` is not empty (`Set.Nonempty s`), then `a` is less than or equal to the infimum of set `s` (`a ≤ sInf s`) if and only if `a` is less than or equal to every element in the set `s` (i.e., `∀ b ∈ s, a ≤ b`).
More concisely: For any conditionally complete linear order type `α` with a lowest element, an non-empty set `s` of `α`, and an element `a` of `α`, `a ≤ sInf s` if and only if `a ≤ b` for all `b ∈ s`.
|
csSup_image2_eq_csSup_csSup
theorem csSup_image2_eq_csSup_csSup :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α]
[inst_1 : ConditionallyCompleteLattice β] [inst_2 : ConditionallyCompleteLattice γ] {s : Set α} {t : Set β}
{l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β},
(∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) →
(∀ (a : α), GaloisConnection (l a) (u₂ a)) →
s.Nonempty → BddAbove s → t.Nonempty → BddAbove t → sSup (Set.image2 l s t) = l (sSup s) (sSup t)
This theorem states that for any types `α`, `β`, `γ` equipped with the structure of a conditionally complete lattice, and for any sets `s` of type `α` and `t` of type `β`, along with the binary function `l : α → β → γ` and the functions `u₁ : β → γ → α` and `u₂ : α → γ → β` satisfying certain Galois connection properties, if `s` and `t` are nonempty and bounded above, then the supremum of the image (under `l`) of the cartesian product of `s` and `t` is equal to the result of applying `l` to the supremum of `s` and the supremum of `t`. In other words, the supremum operation can be interchanged with the binary function `l` under these conditions.
More concisely: Given types `α`, `β`, `γ` with the structure of conditionally complete lattices, and sets `s` of type `α` and `t` of type `β` that are nonempty and bounded above, if functions `l : α → β → γ`, `u₁ : β → γ → α`, and `u₂ : α → γ → β` satisfy Galois connection properties, then the supremum of `l(s × t)` equals `l(sup s sup t)`.
|
ciInf_mono
theorem ciInf_mono :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {f g : ι → α},
BddBelow (Set.range f) → (∀ (x : ι), f x ≤ g x) → iInf f ≤ iInf g
The theorem `ciInf_mono` states that for any type `α` that forms a conditionally complete lattice and any two functions `f` and `g` from an arbitrary index type `ι` to `α`, if the set of all values (the range) of the function `f` is bounded below and every element of the index type `ι` maps to a value in `g` greater than or equal to the corresponding value in `f` (i.e., `f` and `g` are pointwise comparable), then the infimum (the greatest lower bound) of the set of all values of `f` is less than or equal to the infimum of the set of all values of `g`.
More concisely: If `α` is a conditionally complete lattice and `f` and `g` are pointwise comparable functions from an index type `ι` to `α` with `f` having a bottom element and the range of `g` containing the infimum of the range of `f`, then `inf(range(g)) ≤ inf(range(f))`.
|
IsGreatest.csSup_eq
theorem IsGreatest.csSup_eq :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α}, IsGreatest s a → sSup s = a := by
sorry
The theorem `IsGreatest.csSup_eq` states that for any type `α` which is a conditionally complete lattice, and for any set `s` of type `α` and an element `a` of type `α`, if `a` is the greatest element of the set `s`, then the supremum (`sSup`) of the set `s` is equal to `a`. This means that in a conditionally complete lattice, the greatest element of a set is always equal to the supremum of the set.
More concisely: In a conditionally complete lattice, the greatest element of a set is equal to its supremum.
|
exists_lt_of_csInf_lt
theorem exists_lt_of_csInf_lt :
∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} {b : α},
s.Nonempty → sInf s < b → ∃ a ∈ s, a < b
The theorem `exists_lt_of_csInf_lt` states that for any type `α` with a conditionally complete linear order, and for any set `s` of `α` and arbitrary element `b` of `α`, if `s` is nonempty and the infimum of `s` is less than `b`, then there exists an element `a` in `s` such that `a` is less than `b`. In other words, if the greatest lower bound of a nonempty set is less than some value, there's an element in the set that's also less than that value.
More concisely: For any nonempty set `s` with infimum in a conditionally complete linear order `α`, if the infimum of `s` is strictly less than some `b` in `α`, then there exists `a` in `s` with `a` strictly less than `b`.
|
ciSup_eq_of_forall_le_of_forall_lt_exists_gt
theorem ciSup_eq_of_forall_le_of_forall_lt_exists_gt :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {b : α} [inst_1 : Nonempty ι] {f : ι → α},
(∀ (i : ι), f i ≤ b) → (∀ w < b, ∃ i, w < f i) → ⨆ i, f i = b
This theorem, `ciSup_eq_of_forall_le_of_forall_lt_exists_gt`, states that for any type `α` that forms a conditionally complete lattice, and given any function `f` from a nonempty type `ι` to `α`, if `b` is a value in `α` such that `f i` is always less than or equal to `b` for all `i` in `ι`, and for any value `w` that is less than `b`, there exists an `i` such that `w` is less than `f i`, then `b` is the supremum (or least upper bound) of `f`. In other words, `b` is the smallest value that is greater than or equal to all values of `f`, and there is no value less than `b` that has this property. This theorem is a rule that can be used to prove that a value is the supremum of a function in a conditionally complete lattice structure.
More concisely: For any conditionally complete lattice `α` and function `f` from a nonempty type `ι` to `α`, if for all `i` in `ι`, `f i` is less than or equal to `b`, and for every `w` less than `b`, there exists an `i` with `w` less than `f i`, then `b` is the supremum (least upper bound) of `f`.
|
WithTop.iSup_coe_eq_top
theorem WithTop.iSup_coe_eq_top :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] {f : ι → α},
⨆ x, ↑(f x) = ⊤ ↔ ¬BddAbove (Set.range f)
The theorem `WithTop.iSup_coe_eq_top` states that for any types `α` and `ι`, given a conditionally complete linear order with a bottom for `α` and a function `f` from `ι` to `α`, the supremum of the co-domain of `f` is equal to the top element if and only if the range of `f` is not bounded above. In other words, the supremum of the image of `f` over all `ι` being infinity implies that there is no upper bound for the set of all possible values of `f`.
More concisely: For any conditionally complete linear order with a bottom, a function from an index type to the order's type, and an unbounded range, the supremum of the function's image equals the top element.
|
csInf_eq_of_forall_ge_of_forall_gt_exists_lt
theorem csInf_eq_of_forall_ge_of_forall_gt_exists_lt :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {b : α},
s.Nonempty → (∀ a ∈ s, b ≤ a) → (∀ (w : α), b < w → ∃ a ∈ s, a < w) → sInf s = b
This theorem, `csInf_eq_of_forall_ge_of_forall_gt_exists_lt`, states that for any type 'α' that is a conditionally complete lattice, any set 's' of type 'α', and any element 'b' of type 'α', if the set 's' is not empty, and 'b' is less than or equal to every element in 's', and for any element 'w' from 'α' where 'b' is less than 'w' there exists an element 'a' in the set 's' that is less than 'w', then 'b' is the greatest lower bound (infimum) of the set 's'. In other words, 'b' is the largest value that is less than or equal to every element in 's'.
This theorem is useful for proving that a certain value is the greatest lower bound of a set in a conditionally complete lattice, which is a partially ordered set in which any non-empty subset that has an upper bound, has a least upper bound (supremum), and any non-empty subset that has a lower bound, has a greatest lower bound (infimum).
More concisely: If 'α' is a conditionally complete lattice, and 's' is a non-empty subset of 'α' with lower bound 'b' such that 'b' is less than or equal to every 'x' in 's' and for every 'w' with 'b' < 'w' there exists an 'a' in 's' with 'a' < 'w', then 'b' is the greatest lower bound (infimum) of 's'.
|
isLeast_csInf
theorem isLeast_csInf :
∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α}
[inst_1 : IsWellOrder α fun x x_1 => x < x_1], s.Nonempty → IsLeast s (sInf s)
The theorem `isLeast_csInf` states that for any type `α` that has a conditionally complete linear order, and for any set `s` of type `α` that is well-ordered under the strict less than relation, if the set `s` is nonempty then the infimum (greatest lower bound) of `s` is the least element of `s`. In other words, the infimum of `s` belongs to `s` and is less than or equal to every other element in `s`. The conditionally complete linear order ensures that every nonempty set `s`, which is bounded from below, has an infimum, and the well-ordering guarantees that there is a least element in `s`.
More concisely: For any nonempty well-ordered set `s` in a conditionally complete linear order `α`, the infimum of `s` is the least element of `s`.
|
le_ciSup
theorem le_ciSup :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {f : ι → α},
BddAbove (Set.range f) → ∀ (c : ι), f c ≤ iSup f
The theorem `le_ciSup` states that for any type `α` equipped with a `ConditionallyCompleteLattice` structure, and for any function `f` from the type `ι` to `α`, if the range of `f` is bounded above, then the value of `f` at any point `c` from `ι` is less than or equal to the supremum of `f` over its domain. In other words, the supremum of the function, denoted as `iSup f`, acts as an upper bound for the values of `f` at all points from the domain `ι`.
More concisely: For any function `f` from a type `ι` to a conditionally complete lattice `α`, if `f` has a supremum, then for all `c` in `ι`, we have `f c ≤ iSup f`.
|
csSup_eq_csSup_of_forall_exists_le
theorem csSup_eq_csSup_of_forall_exists_le :
∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s t : Set α},
(∀ x ∈ s, ∃ y ∈ t, x ≤ y) → (∀ y ∈ t, ∃ x ∈ s, y ≤ x) → sSup s = sSup t
The theorem `csSup_eq_csSup_of_forall_exists_le` states that for all sets `s` and `t` of a specific type `α` that has a conditionally complete linear order, if every element `x` in `s` is bounded by some element `y` in `t`, and likewise, every element `y` in `t` is bounded by some element `x` in `s`, then the supremum of `s` (greatest element) is equal to the supremum of `t`. This is true even when the sets are empty or unbounded.
More concisely: If sets `s` and `t` of a conditionally complete linear order `α` have the property that every element of `s` is bounded by some element of `t` and vice versa, then `sup s = sup t`.
|
le_csInf_inter
theorem le_csInf_inter :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s t : Set α},
BddBelow s → BddBelow t → (s ∩ t).Nonempty → sInf s ⊔ sInf t ≤ sInf (s ∩ t)
The theorem `le_csInf_inter` states that for any two sets `s` and `t` of elements of a conditionally complete lattice `α`, if both `s` and `t` are bounded below and their intersection is nonempty, then the infimum (greatest lower bound) of the intersection of `s` and `t` is greater than or equal to the maximum of the infima of `s` and `t`. In mathematical terms, if $\inf s$ and $\inf t$ are the infima of the sets `s` and `t` respectively, then $\inf (s \cap t) \geq \max(\inf s, \inf t)$.
More concisely: If `s` and `t` are nonempty, bounded below sets in a conditionally complete lattice `α`, then the infimum of their intersection is greater than or equal to the greater of the infima of `s` and `t`. In mathematical notation, $\inf (s \cap t) \geq \max(\inf s, \inf t)$.
|
csInf_eq_csInf_of_forall_exists_le
theorem csInf_eq_csInf_of_forall_exists_le :
∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s t : Set α},
(∀ x ∈ s, ∃ y ∈ t, y ≤ x) → (∀ y ∈ t, ∃ x ∈ s, x ≤ y) → sInf s = sInf t
The theorem `csInf_eq_csInf_of_forall_exists_le` states that for any type `α` that has a conditionally complete linear order, and for any two sets `s` and `t` of elements of `α`, if every element `x` in set `s` has an element `y` in set `t` such that `y` is less than or equal to `x` and vice versa, then the infimum of `s` is equal to the infimum of `t`. This is true even if the sets `s` or `t` are empty or unbounded. Here, the infimum of a set is the greatest element that is less than or equal to all elements of the set.
More concisely: If `α` is a conditionally complete linear order type and `s` and `t` are sets of `α` such that for all `x in s` there exists `y in t` with `x ≤ y` and vice versa, then `inf s = inf t`.
|
WithTop.coe_sSup
theorem WithTop.coe_sSup :
∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α}, BddAbove s → ↑(sSup s) = ⨆ a ∈ s, ↑a
The theorem `WithTop.coe_sSup` asserts that for any type `α` endowed with a structure of a conditionally complete linear order with a bottom element, and any set `s` of elements of type `α`, if `s` is bounded above then the supremum (`sSup`) of `s` cast to the extended type `WithTop α` is equal to the supremum over the elements of `s` cast to `WithTop α`. In other words, taking the supremum within `α` and then extending to `WithTop α` is the same as extending the elements to `WithTop α` first and then taking the supremum.
More concisely: For any conditionally complete linearly ordered type `α` with a bottom element and any bounded above subset `s` of `α`, the supremum of `s` in `WithTop α` is equal to the supremum of the elements of `s` extended to `WithTop α`.
|
ConditionallyCompleteLattice.le_csSup
theorem ConditionallyCompleteLattice.le_csSup :
∀ {α : Type u_5} [self : ConditionallyCompleteLattice α] (s : Set α) (a : α), BddAbove s → a ∈ s → a ≤ sSup s := by
sorry
The theorem `ConditionallyCompleteLattice.le_csSup` states that for any type `α`, which forms a conditionally complete lattice, and for any set `s` of this type and any element `a` of this set, if `s` is bounded above then `a` is less than or equal to the supremum of `s`, denoted by `sSup s`. In other words, all elements of a set that has an upper bound are less than or equal to the supremum of the set in a conditionally complete lattice.
More concisely: In a conditionally complete lattice, any element is less than or equal to the supremum of a bounded above subset.
|
csSup_singleton
theorem csSup_singleton : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] (a : α), sSup {a} = a
This theorem states that for any type `α` that forms a Conditionally Complete Lattice, the supremum (least upper bound) of a singleton set (a set with only one element `a`) is equal to the element `a` itself. In other words, when the set has only one element, that element is both the least and greatest element in the set.
More concisely: For any type `α` forming a Conditionally Complete Lattice, the supremum of a singleton set `{a}` is equal to `a`.
|
GaloisConnection.l_ciSup
theorem GaloisConnection.l_ciSup :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α]
[inst_1 : ConditionallyCompleteLattice β] [inst_2 : Nonempty ι] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ {f : ι → α}, BddAbove (Set.range f) → l (⨆ i, f i) = ⨆ i, l (f i)
The theorem `GaloisConnection.l_ciSup` states that for all types `α`, `β`, and `ι`, where `α` and `β` are conditionally complete lattices (meaning they are partially ordered sets in which every nonempty, bounded above subset has a least upper bound) and `ι` is nonempty, and for all functions `l : α → β` and `u : β → α` that form a Galois connection (i.e., for every `a : α` and `b : β`, `l a ≤ b` is equivalent to `a ≤ u b`), if the range of a function `f : ι → α` is bounded above, then applying `l` to the supremum (the least upper bound) of the function `f` over all `ι` is equal to the supremum of the function `l ∘ f` (i.e., the function that first applies `f`, then `l`) over all `ι`.
More concisely: For any conditionally complete lattices α, β and nonempty ι, if l : α → β and u : β → α form a Galois connection and the range of f : ι → α is bounded above, then (l (⨆ x : ι, f x)) = ⨆ x : ι, (l (f x)).
|
IsLeast.csInf_eq
theorem IsLeast.csInf_eq :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α}, IsLeast s a → sInf s = a
This theorem states that for any type `α` that forms a conditionally complete lattice, and for any set `s` of elements of type `α`, if there exists a least element `a` in the set `s`, then the infimum (greatest lower bound) of the set `s` is equal to `a`. This means that `a` is the smallest element in `s` that is greater than or equal to all other elements in `s`.
More concisely: For any conditionally complete lattice `α` and set `s` in `α` having a least element `a`, the infimum of `s` equals `a`. In other words, the least element of `s` is the greatest lower bound of `s`.
|
csSup_eq_of_is_forall_le_of_forall_le_imp_ge
theorem csSup_eq_of_is_forall_le_of_forall_le_imp_ge :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {b : α},
s.Nonempty → (∀ a ∈ s, a ≤ b) → (∀ (ub : α), (∀ a ∈ s, a ≤ ub) → b ≤ ub) → sSup s = b
This theorem states that for any nonempty set `s` of elements of a type `α` that has a structure of a conditionally complete lattice, and any element `b` of the same type, if `b` is an upper bound for all elements of `s` (i.e., every element of `s` is less than or equal to `b`), and if for any other upper bound `ub` of `s`, `b` is less than or equal to `ub`, then `b` is the supremum of `s`. In other words, the supremum of a set is the least upper bound.
More concisely: If a nonempty set `s` of elements in a conditionally complete lattice `α` has an upper bound `b`, and `b` is the least upper bound among all upper bounds of `s`, then `b` is the supremum of `s`.
|
ciSup_const
theorem ciSup_const :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] [hι : Nonempty ι] {a : α}, ⨆ x, a = a := by
sorry
This theorem, `ciSup_const`, states that for any type `α` that forms a conditionally complete lattice and any nonempty index set `ι`, the supremum of any constant `a` from `α` over all elements `x` of the index set is equal to the constant `a` itself. This result holds regardless of the specific elements in the index set `ι` and does not require any additional conditions on the constant `a`.
More concisely: For any conditionally complete lattice `α` and nonempty index set `ι`, the supremum of a constant `a` in `α` over all elements of `ι` equals `a`.
|
csSup_inter_le
theorem csSup_inter_le :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s t : Set α},
BddAbove s → BddAbove t → (s ∩ t).Nonempty → sSup (s ∩ t) ≤ sSup s ⊓ sSup t
The theorem `csSup_inter_le` states that for any type `α` that is a Conditionally Complete Lattice, and any two sets `s` and `t` of this type, if both `s` and `t` are bounded above and their intersection is nonempty, then the supremum (least upper bound) of the intersection of `s` and `t` is less than or equal to the infimum (greatest lower bound) of the supremums of `s` and `t`. This essentially means the largest value in the intersection of the two sets is less than or equal to the smaller of the largest values in each of the individual sets, given that these largest values exist.
More concisely: For any Conditionally Complete Lattice type `α`, if `s` and `t` are nonempty, bounded subsets with a common upper bound, then the infimum of their supremums is less than or equal to the supremum of their intersection.
|
csInf_le
theorem csInf_le :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α}, BddBelow s → a ∈ s → sInf s ≤ a := by
sorry
This theorem, `csInf_le`, states that for any type `α` that forms a conditionally complete lattice, for any set `s` of elements of this type, and for any element `a` of this type, if the set `s` is bounded below (i.e., there exists a lower bound for `s`) and if the element `a` is in `s`, then the greatest lower bound (or infimum) of `s`, denoted as `sInf s`, is less than or equal to `a`. In simple terms, it asserts that the infimum of any set that has a lower bound, is always less than or equal to any member of that set.
More concisely: For any conditionally complete lattice type `α`, if `s` is a bounded below set in `α` containing an element `a`, then `sInf s ≤ a`.
|
ConditionallyCompleteLinearOrderBot.csSup_empty
theorem ConditionallyCompleteLinearOrderBot.csSup_empty :
∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrderBot α], sSup ∅ = ⊥
This theorem states that for any type `α` that has a structure of `ConditionallyCompleteLinearOrderBot` (which is a conditionally complete linear order with a bottom element `⊥`), the supremum (or the least upper bound) of an empty set is the bottom element `⊥`. Essentially, if you try to find the least upper bound of no elements, you get the lowest possible value in the order.
More concisely: For any conditionally complete linear order `α` with bottom element `⊥`, the supremum of an empty set equals `⊥`.
|
ciSup_of_empty
theorem ciSup_of_empty :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] [inst_1 : IsEmpty ι] (f : ι → α),
⨆ i, f i = ⊥
This theorem states that for any given type `α` that has a conditionally complete linear order with a least element, and an empty type `ι`, any function `f` from `ι` to `α` will have its supremum equal to the least element of `α` (denoted by `⊥`). Essentially, if we're trying to find the supremum of an empty set in a conditionally complete ordered set, the result is the least element of the set.
More concisely: For any conditionally complete linearly ordered type `α` with a least element `⊥`, the supremum of the empty function domain is equal to `⊥`.
|
exists_lt_of_ciInf_lt
theorem exists_lt_of_ciInf_lt :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] {a : α} [inst_1 : Nonempty ι]
{f : ι → α}, iInf f < a → ∃ i, f i < a
This theorem, named `exists_lt_of_ciInf_lt`, states that for any type `α` with a conditionally complete linear order, a nonempty indexing type `ι`, and a function `f` from `ι` to `α`, if the indexed infimum of `f` is less than some element `a` of type `α`, then there exists an index `i` (of type `ι`) such that the value of `f` at `i` is less than `a`. In simpler terms, if the greatest lower bound of all the values of `f` is less than `a`, then there is some input to `f` that, when applied, gives a value less than `a`.
More concisely: If `α` is a type with a conditionally complete linear order, `ι` is nonempty, `f : ι → α`, and `inf (range f) < a`, then there exists `i ∈ ι` such that `f i < a`.
|
exists_between_of_forall_le
theorem exists_between_of_forall_le :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s t : Set α},
s.Nonempty → t.Nonempty → (∀ x ∈ s, ∀ y ∈ t, x ≤ y) → (upperBounds s ∩ lowerBounds t).Nonempty
The theorem `exists_between_of_forall_le` states that given any two nonempty sets `s` and `t` of a type `α` that forms a conditionally complete lattice, if all elements of set `s` are less than or equal to all elements of set `t`, then there exists an element that is both an upper bound for set `s` and a lower bound for set `t`. In other words, there is an element that lies between these two sets with respect to the lattice ordering.
More concisely: Given two nonempty sets `s` and `t` of a conditionally complete lattice type `α` with `s ≤ t`, there exists an element `x` such that `x ≤ s.inf ∧ s.sup ≤ x`.
|
ConditionallyCompleteLattice.csSup_le
theorem ConditionallyCompleteLattice.csSup_le :
∀ {α : Type u_5} [self : ConditionallyCompleteLattice α] (s : Set α) (a : α),
s.Nonempty → a ∈ upperBounds s → sSup s ≤ a
The theorem `ConditionallyCompleteLattice.csSup_le` states that for any type `α` that has a conditionally complete lattice structure, any set `s` of `α`, and any element `a` of `α`, if `s` is not empty and `a` is an upper bound of `s`, then the supremum (i.e., the least upper bound) of `s` is less than or equal to `a`. In other words, any upper bound of a set is greater than or equal to the supremum of that set, provided the set is nonempty.
More concisely: For any conditionally complete lattice `α`, if `s` is a nonempty subset of `α` and `a` is an upper bound of `s`, then the supremum of `s` is less than or equal to `a`.
|
OrderIso.map_ciInf
theorem OrderIso.map_ciInf :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α]
[inst_1 : ConditionallyCompleteLattice β] [inst_2 : Nonempty ι] (e : α ≃o β) {f : ι → α},
BddBelow (Set.range f) → e (⨅ i, f i) = ⨅ i, e (f i)
This theorem states that for any types `α` and `β`, and for any index type `ι` such that `α` and `β` are both conditionally complete lattices and `ι` is nonempty, if we have an order-preserving bijection `e` from `α` to `β` and a function `f` from `ι` to `α` whose range is bounded below, then the image under `e` of the infimum (greatest lower bound) over all `i` of `f(i)` is equal to the infimum over all `i` of the image under `e` of `f(i)`. In other words, the order-preserving bijection `e` commutes with taking infima over a lower-bounded range.
More concisely: Given order-preserving bijections between conditionally complete lattices `α`, `β`, index type `ι` with a nonempty range, and a function `f : ι → α` whose range is bounded below, the infimum of `e(f(i))` over `i` equals `e` of the infimum of `f(i)`.
In other words, `e(⨧ i in ι (f i)) = ⨧ i in ι (e (f i))` where `⨧` denotes the infimum (greatest lower bound) operator.
|
ConditionallyCompleteLinearOrderBot.bot_le
theorem ConditionallyCompleteLinearOrderBot.bot_le :
∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrderBot α] (x : α), ⊥ ≤ x
This theorem states that in any conditionally complete linear order with a least element (denoted by `⊥`), this least element is less than or equal to any element `x` of the set. In other words, `⊥` is the smallest value in the order.
More concisely: In any conditionally complete linear order with a least element, the least element is less than or equal to every other element.
|
isLUB_ciSup
theorem isLUB_ciSup :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] [inst_1 : Nonempty ι] {f : ι → α},
BddAbove (Set.range f) → IsLUB (Set.range f) (⨆ i, f i)
The theorem `isLUB_ciSup` states that for any type `α` which is a conditionally complete lattice, and for any non-empty type `ι`, given a function `f` from `ι` to `α`, if the range of the function `f` is bounded above, then the least upper bound (supremum) of the set that is the range of `f` is equal to the supremum over all `i` of `f(i)`. In other words, if a set of values derived from a function is bounded above, then the least upper bound of this set is equivalent to the supremum of the function's output values.
More concisely: For any conditionally complete lattice α and non-empty ι, if function f from ι to α has a bounded above range, then the supremum of f is equal to the supremum of its values.
|
csSup_le_csSup
theorem csSup_le_csSup :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s t : Set α},
BddAbove t → s.Nonempty → s ⊆ t → sSup s ≤ sSup t
This theorem states that for any type `α` that forms a conditionally complete lattice and for any two sets `s` and `t` of type `α`, if `t` is bounded above, and `s` is not empty, and every element of `s` is also an element of `t` (i.e., `s` is a subset of `t`), then the supremum (least upper bound) of `s` is less than or equal to the supremum of `t`. In simpler terms, the least upper bound of a non-empty subset of a bounded set does not exceed the least upper bound of the whole set.
More concisely: Let `α` be a conditionally complete lattice, `s` and `t` be non-empty sets of type `α`, and `t` be bounded above. If `s` is a subset of `t`, then the supremum of `s` is less than or equal to the supremum of `t`.
|
lt_csSup_of_lt
theorem lt_csSup_of_lt :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a b : α},
BddAbove s → a ∈ s → b < a → b < sSup s
The theorem `lt_csSup_of_lt` states that for any set `s` of elements of a type `α` that forms a conditionally complete lattice, and for any elements `a` and `b` of `α`, if `s` is bounded above, `a` is an element of `s`, and `b` is less than `a`, then `b` is less than the supremum of `s`. This is essentially an "if and only if" statement, however, the assumptions for the two implications are slightly different (one requires the set to be bounded above for one direction, while the other requires the set to be nonempty and have a linear order), so we state the two implications separately, as opposed to what we would do in the case of a complete lattice.
More concisely: If `s` is a conditionally complete lattice, `a` is in `s`, `b` is in `s` and less than `a`, and `s` is bounded above, then `b` is less than the supremum of `s`.
|
ciSup_unique
theorem ciSup_unique :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] [inst_1 : Unique ι] {s : ι → α},
⨆ i, s i = s default
This theorem states that for any type `α` which forms a conditionally complete lattice, and another type `ι` with a unique element, then the supremum (denoted by ⨆) of a function `s : ι → α` over all elements of `ι` is equal to the value of `s` at the default element of `ι`. This makes sense intuitively, as if there is only one element in `ι`, then the supremum of the function values over all `ι` should be just the function value at that unique element.
More concisely: For any conditionally complete lattice `α` and type `ι` with a unique element, the supremum of a function `s : ι → α` is equal to `s!0`, where `!` denotes the unique element operator.
|
WithTop.coe_sInf
theorem WithTop.coe_sInf :
∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α}, s.Nonempty → ↑(sInf s) = ⨅ a ∈ s, ↑a
This theorem, named `WithTop.coe_sInf`, states that for any type `α` that has the structure of a conditionally complete linear order with a bottom element, and any non-empty set `s` of elements of type `α`, the infimum (greatest lower bound) of the set `s`, when lifted to the type with an added top element, equals the infimum of the elements of `s` lifted individually to the type with an added top element. In other words, finding the smallest element of `s` first and then lifting it to the extended type is the same as first lifting each element of `s` to the extended type and then finding the smallest element.
More concisely: For any conditionally complete linearly ordered type `α` with a bottom element and non-empty set `s` of elements, the infimum of `s` with the top element coerced is equal to the coerced infimum of the elements in `s`.
|
IsLUB.csSup_eq
theorem IsLUB.csSup_eq :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α}, IsLUB s a → s.Nonempty → sSup s = a
This theorem states that for any type `α` which is a conditionally complete lattice, any set `s` of type `α`, and any element `a` of type `α`, if `a` is a least upper bound of the set `s` and the set `s` is not empty, then the supremum of the set `s` is equal to `a`. In other words, it ensures that in a conditionally complete lattice, the supremum of a non-empty set, if it exists, is its unique least upper bound.
More concisely: In a conditionally complete lattice, if a non-empty set has a least upper bound, then its least upper bound is unique and equals the supremum of the set.
|
ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove
theorem ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove :
∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrder α] (s : Set α), ¬BddAbove s → sSup s = sSup ∅
This theorem states that for any type `α` that has a conditionally complete linear order, if a set `s` of type `α` is not bounded above, then the supremum (least upper bound) of this set `s` is conventionally the supremum of the empty set. In other words, if no upper bound exists for a given set, the least upper bound of the set is defined to be the least upper bound of an empty set.
More concisely: If a type `α` with a conditional complete linear order has no upper bound for set `s`, then the supremum of `s` equals the supremum of the empty set.
|
csSup_union
theorem csSup_union :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s t : Set α},
BddAbove s → s.Nonempty → BddAbove t → t.Nonempty → sSup (s ∪ t) = sSup s ⊔ sSup t
The theorem `csSup_union` states that for any type `α` that has a structure of a `ConditionallyCompleteLattice`, and for any two sets `s` and `t` of this type, if both sets are bounded above and nonempty, then the supremum of the union of `s` and `t` is equal to the maximum of the suprema of `s` and `t`. Here, the supremum of a set is the least upper bound of the set, and `⊔` represents the operation of taking the maximum of two elements in the lattice.
More concisely: For any conditionally complete lattice type `α`, if `s` and `t` are nonempty, bounded above sets, then `sup (s ∪ t) = sup s ⊔ sup t`.
|
exists_lt_of_lt_ciSup
theorem exists_lt_of_lt_ciSup :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] {b : α} [inst_1 : Nonempty ι]
{f : ι → α}, b < iSup f → ∃ i, b < f i
This theorem, named `exists_lt_of_lt_ciSup`, is an indexed version of an existing lemma `exists_lt_of_lt_csSup`. It states that for any type `α` with a conditionally complete linear order, a type `ι` that is nonempty, a value `b` of type `α`, and a function `f` mapping from `ι` to `α`, if `b` is less than the supremum of the set of all images of `f` (noted as `iSup f`), then there exists an element `i` in `ι` such that `b` is less than the image of `i` under `f` (noted as `f i`). In mathematical notation, if $b < \sup_{i\in I} f(i)$, then there exists an $i$ in $I$ such that $b < f(i)$.
More concisely: If `α` is a type with a conditionally complete linear order, `ι` is nonempty, `b` is in `α`, and `f` maps `ι` to `α` with `b` less than the supremum of `f`'s images, then there exists an `i` in `ι` such that `b` is less than `f(i)`.
|
csSup_of_not_bddAbove
theorem csSup_of_not_bddAbove :
∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α}, ¬BddAbove s → sSup s = sSup ∅
This theorem states that for any type `α` that is a conditionally complete linear order and for any set `s` of type `α`, if `s` is not bounded above, then the supremum (least upper bound) of `s` is equal to the supremum of the empty set.
In mathematical terms, if there does not exist an upper bound for the set `s`, the least upper bound of `s` is equal to the least upper bound of the empty set. This theorem is a statement about the properties of boundedness and the supremum in a conditionally complete linear order.
More concisely: In a conditionally complete linear order, if a set has no upper bound, then its supremum equals the supremum of the empty set.
|
ConditionallyCompleteLinearOrder.le_total
theorem ConditionallyCompleteLinearOrder.le_total :
∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrder α] (a b : α), a ≤ b ∨ b ≤ a
This theorem states that in the context of a `ConditionallyCompleteLinearOrder`, which is an ordered set in which every nonempty set that has an upper bound also has a least upper bound, for any two elements `a` and `b` of an arbitrary type `α`, one of two conditions must hold: either `a` is less than or equal to `b`, or `b` is less than or equal to `a`. This property is also known as total order or linearity.
More concisely: In a ConditionallyCompleteLinearOrder, any two elements are either related by the total order relation or equal.
|
exists_lt_of_lt_csSup
theorem exists_lt_of_lt_csSup :
∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} {b : α},
s.Nonempty → b < sSup s → ∃ a ∈ s, b < a
The theorem `exists_lt_of_lt_csSup` states that for any type `α` that has a conditionally complete linear order, any non-empty set `s` of type `α`, and any element `b` of type `α`, if `b` is strictly less than the supremum of `s` (denoted `sSup s`), then there exists an element `a` in `s` such that `b` is strictly less than `a`. This theorem essentially captures one of the properties of the supremum of a set in the context of a linear order.
More concisely: If `α` is a conditionally complete linear order, `s` is a non-empty subset of `α`, and `b` is strictly less than the supremum of `s`, then there exists an `a` in `s` such that `b` is strictly less than `a`.
|
csInf_union
theorem csInf_union :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s t : Set α},
BddBelow s → s.Nonempty → BddBelow t → t.Nonempty → sInf (s ∪ t) = sInf s ⊓ sInf t
The theorem `csInf_union` states that for any type `α` that forms a conditionally complete lattice, and any two sets `s` and `t` of type `α`, if both `s` and `t` are bounded below and nonempty, then the greatest lower bound (infimum) of the union of `s` and `t` is equal to the infimum of `s` intersected with the infimum of `t`. This expresses a sort of distributive property for the infimum function over the union of two sets.
More concisely: For any conditionally complete lattice type `α`, if `s` and `t` are nonempty, bounded below sets, then `inf (s ∪ t) = inf (s) ∧ inf (t)`.
|
le_ciSup_of_le
theorem le_ciSup_of_le :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {a : α} {f : ι → α},
BddAbove (Set.range f) → ∀ (c : ι), a ≤ f c → a ≤ iSup f
This theorem states that for any type `α` with a conditionally complete lattice structure, a type `ι`, an `α`-valued function `f` mapping elements of type `ι`, and an element `a` of type `α`, if the range of the function `f` is bounded above, then for any element `c` of type `ι`, if `a` is less than or equal to `f(c)`, then `a` is also less than or equal to the supremum of the set of values that `f` can take. This supremum is obtained by first getting the range of the function `f` and then applying the supremum operation to this range.
More concisely: For any conditionally complete lattice `α` and function `f` from type `ι` to `α` with a bounded above range, if `a ≤ f(c)` for some `c ∈ ι`, then `a ≤ sup (rang(f))`.
|
ciSup_le'
theorem ciSup_le' :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] {f : ι → α} {a : α},
(∀ (i : ι), f i ≤ a) → ⨆ i, f i ≤ a
This theorem states that for any type `α` under the condition that it is a conditionally complete linear order with a least element (also known as a "bottom"), a function `f` from some type `ι` to `α`, and a specific element `a` of type `α`, if all values of `f(i)` are less than or equal to `a` for any `i` of type `ι`, then the supremum (or least upper bound) of the set of all `f(i)` (symbolized by `⨆ i, f i`) is also less than or equal to `a`. Essentially, if every value a function produces is less than or equal to a certain number, then the maximum value that function can produce is also less than or equal to that number.
More concisely: If `α` is a conditionally complete linear order with a least element, and `f: ι → α` is a function such that `f i ≤ a` for all `i`, then `⨆ i, f i ≤ a`.
|
ConditionallyCompleteLattice.le_csInf
theorem ConditionallyCompleteLattice.le_csInf :
∀ {α : Type u_5} [self : ConditionallyCompleteLattice α] (s : Set α) (a : α),
s.Nonempty → a ∈ lowerBounds s → a ≤ sInf s
This theorem states that for any given set `s` of a type `α` that forms a Conditionally Complete Lattice, and for any element `a` of this type `α`, if `s` is non-empty and `a` is an element of the set of lower bounds of `s`, then `a` is less than or equal to the greatest lower bound (`sInf`) of the set `s`.
In simpler terms, it says for any non-empty set in a conditionally complete lattice, any element that is a lower bound of this set is not greater than the greatest lower bound of that set.
More concisely: For any non-empty conditionally complete lattice `s` of type `α` and any lower bound `a` of `s`, we have `a ≤ s.inf`.
|
WithTop.coe_sInf'
theorem WithTop.coe_sInf' :
∀ {α : Type u_1} [inst : InfSet α] {s : Set α}, s.Nonempty → ↑(sInf s) = sInf ((fun a => ↑a) '' s)
The theorem `WithTop.coe_sInf'` states that for any type `α` which has an infimum operation defined on its set of instances (`InfSet α`), and any non-empty set `s` of type `α`, the infimum of `s` when considered as an element of `WithTop α` (denoted by `↑(sInf s)`) is equal to the infimum of the image of `s` under the function that maps each element to an element of `WithTop α`. In other words, embedding the infimum of a non-empty set into `WithTop α` preserves the value of the infimum.
More concisely: For any non-empty set `s` in a type `α` with an infimum operation, the infimum of `s` in `WithTop α` is equal to the infimum of the image of `s` under the function mapping elements to their `WithTop α` counterparts.
|
csSup_insert
theorem csSup_insert :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α},
BddAbove s → s.Nonempty → sSup (insert a s) = a ⊔ sSup s
The theorem `csSup_insert` states that for any set `s` of a certain type `α`, where `α` forms a conditionally complete lattice, and for any element `a` of the same type `α`, if `s` is nonempty and has an upper bound, the supremum (least upper bound) of the set that results from inserting `a` into `s` is the maximum of `a` and the supremum of `s`. In mathematical terms, this can be written as $\sup(a \cup s) = \max\{a, \sup s\}$.
More concisely: The supremum of a nonempty set `s` in a conditionally complete lattice, together with an upper bound, equals the maximum of the new element `a` and the supremum of `s`, i.e., $\sup(a \cup s) = \max\{a, \sup s\}$.
|
WithTop.isLUB_sSup'
theorem WithTop.isLUB_sSup' :
∀ {β : Type u_5} [inst : ConditionallyCompleteLattice β] {s : Set (WithTop β)}, s.Nonempty → IsLUB s (sSup s) := by
sorry
The theorem `WithTop.isLUB_sSup'` states that for any non-empty set `s` of an arbitrary type `β` that is structured as a conditionally complete lattice with a top, the supremum (`sSup`) of `s` serves as its least upper bound. This means that the `sSup` of `s` is an upper bound of `s` and any other upper bound of `s` is greater than or equal to this `sSup`.
More concisely: For any non-empty set `s` in a conditionally complete lattice with a top element, the supremum of `s` is the least upper bound of `s`.
|
isLUB_csSup
theorem isLUB_csSup :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α}, s.Nonempty → BddAbove s → IsLUB s (sSup s)
The theorem `isLUB_csSup` states that for any type `α` that has the structure of a conditionally complete lattice, if we have a non-empty set `s` of elements of type `α`, that is bounded above, then the supremum of the set `s` (`sSup s`) is a least upper bound of the set `s`. In other words, for every non-empty `s` that has an upper bound, there doesn't exist any other upper bound which is less than the supremum of `s`.
More concisely: If `α` is a conditionally complete lattice and `s` is a non-empty, bounded above subset of `α`, then `sSup s` is the least upper bound of `s`.
|
ciInf_eq_of_forall_ge_of_forall_gt_exists_lt
theorem ciInf_eq_of_forall_ge_of_forall_gt_exists_lt :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {b : α} [inst_1 : Nonempty ι] {f : ι → α},
(∀ (i : ι), b ≤ f i) → (∀ (w : α), b < w → ∃ i, f i < w) → ⨅ i, f i = b
This theorem states that for any type `α` which forms a conditionally complete lattice and any type `ι`, if `b` is an element of `α` and `f` is a function from `ι` to `α`, then `b` is the infimum of `f` if and only if `b` is less than or equal to `f i` for all `i` in `ι`, and for all `w` in `α` where `b` is less than `w`, there exists an `i` such that `f i` is less than `w`. This theorem essentially provides a characterization of the infimum (greatest lower bound) of a function in a conditionally complete lattice.
More concisely: For any conditionally complete lattice `α` and function `f` from a type `ι` to `α`, an element `b` is the infimum of `f` if and only if `b` is less than or equal to `f i` for all `i` in `ι`, and for every `w` in `α` with `b` less than `w`, there exists an `i` such that `w` is less than `f i`.
|
GaloisConnection.l_csSup
theorem GaloisConnection.l_csSup :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst_1 : ConditionallyCompleteLattice β]
{l : α → β} {u : β → α}, GaloisConnection l u → ∀ {s : Set α}, s.Nonempty → BddAbove s → l (sSup s) = ⨆ x, l ↑x
This theorem states that for any conditionally complete lattices `α` and `β`, and a pair of functions `l : α → β` and `u : β → α` that form a Galois connection, if we have a non-empty set `s` of `α` that is bounded above, then the value of function `l` at the supremum of set `s` is equal to the supremum of the set obtained by applying function `l` to each element of `s`. In essence, this theorem is asserting that in the context of a Galois connection, the function `l` preserves the operation of taking supremum from set `s` to the image set under function `l`.
More concisely: Given any conditionally complete lattices `α` and `β`, and a Galois connection `l : α → β` and `u : β → α`, if `s` is a non-empty bounded above subset of `α`, then `l (sup s) = sup (map l s)`.
|
csSup_le_iff'
theorem csSup_le_iff' :
∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α},
BddAbove s → ∀ {a : α}, sSup s ≤ a ↔ ∀ x ∈ s, x ≤ a
The theorem `csSup_le_iff'` states that for every type `α` with a conditionally complete linear order (including a bottom element), and for every set `s` of elements of type `α`, if the set `s` is bounded above, then the supremum of `s` is less than or equal to a given element `a` if and only if every element `x` in `s` is less than or equal to `a`. In other words, it gives a characterization for when a certain element `a` is an upper bound for the set `s` in terms of the supremum of `s`.
More concisely: For any type `α` with a conditionally complete linear order and a set `s` of elements from `α` that has a supremum, `csSup_le_iff'` asserts that `sup s ≤ a` if and only if `x ≤ a` for all `x ∈ s`.
|
WithTop.coe_sSup'
theorem WithTop.coe_sSup' :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SupSet α] {s : Set α},
BddAbove s → ↑(sSup s) = sSup ((fun a => ↑a) '' s)
This theorem states that for any set `s` of a type `α` which has a pre-order and a supremum operation defined on it, if `s` is bounded above, then the supremum (`sSup`) of the elements of `s` taken as elements of the type `WithTop α` (which includes an element "top" greater than all elements of `α`) is equal to the supremum of the set obtained by mapping each element of `s` to the corresponding element of `WithTop α`. In other words, taking the supremum after lifting to `WithTop α` gives the same result as lifting to `WithTop α` first and then taking the supremum, provided that `s` is bounded above.
More concisely: If `s` is a bounded above set with a pre-order and supremum operation in type `α`, then the supremum of `s` in `WithTop α` is equal to the supremum of the images of `s` in `WithTop α`.
|
ciInf_le_of_le
theorem ciInf_le_of_le :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {a : α} {f : ι → α},
BddBelow (Set.range f) → ∀ (c : ι), f c ≤ a → iInf f ≤ a
The theorem `ciInf_le_of_le` states that for any type `α` which is a conditionally complete lattice, given a function `f` that maps from an arbitrary type `ι` to `α`, if the range of the function `f` is bounded below, then for any element `c` from `ι`, if `f(c)` is less than or equal to some element `a` in `α`, it follows that the infimum of the range of `f` is less than or equal to `a`. In essence, if a function's range has a lower bound and any element in the range is less than or equal to a certain value, the infimum of the function's range also falls below or at that value.
More concisely: If `f : ι → α` is a function with domain `ι` and range in a conditionally complete lattice `α`, and `∃ a ∈ α. ∀ i ∈ ι. f i ≤ a`, then `∧ x ∈ range(f) x ≤ a` implies `∧ y ∈ α. inf(range(f)) ≤ y` whenever `inf(range(f))` is defined.
|
OrderIso.map_ciSup
theorem OrderIso.map_ciSup :
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α]
[inst_1 : ConditionallyCompleteLattice β] [inst_2 : Nonempty ι] (e : α ≃o β) {f : ι → α},
BddAbove (Set.range f) → e (⨆ i, f i) = ⨆ i, e (f i)
This theorem states that for every types `α`, `β` and `ι`, where `α` and `β` are conditionally complete lattices and `ι` is nonempty, for every order isomorphism `e` between `α` and `β`, and for every function `f` from `ι` to `α`, if the range of `f` is bounded above, then the order isomorphism `e` applied to the supremum (denoted as `⨆ i, f i`) of `f`, is equal to the supremum of the image of `f` under `e`. In other words, if `f`'s outputs have an upper bound, the order isomorphism preserves the supremum operation.
More concisely: For order isomorphisms between conditionally complete lattices, if a function with a bounded range is applied, the order isomorphism preserves the supremum of the function's images.
|
csSup_empty
theorem csSup_empty : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α], sSup ∅ = ⊥
This theorem states that, for any type `α` that is a conditionally complete linear order with a least element (denoted as `⊥`), the supremum (least upper bound) of an empty set is equal to this least element `⊥`. This is a property of order theory: the supremum of an empty set is the smallest possible element in the set's underlying order.
More concisely: For any conditionally complete linear order `α` with least element `⊥`, the supremum of an empty set equals `⊥`.
|
csInf_insert
theorem csInf_insert :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α},
BddBelow s → s.Nonempty → sInf (insert a s) = a ⊓ sInf s
The theorem `csInf_insert` states that for any type `α` that forms a conditionally complete lattice, any set `s` of type `α`, and any element `a` of type `α`, if the set `s` is nonempty and has a lower bound, then the infimum (greatest lower bound) of the set obtained by inserting the element `a` into the set `s` is equal to the infimum of `a` and the infimum of `s`. In mathematical terms, this could be written as $\inf(a \cup s) = min\{a, \inf s\}$ if $s$ is nonempty and bounded below.
More concisely: If `α` is a conditionally complete lattice, `s` is a nonempty, bounded below set of `α`, and `a` is an element of `α`, then `inf (a :: s) = min {a, inf s}`.
|
csInf_mem
theorem csInf_mem :
∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α}
[inst_1 : IsWellOrder α fun x x_1 => x < x_1], s.Nonempty → sInf s ∈ s
The theorem `csInf_mem` states that for any type `α` that has a conditionally complete linear order, and for any set `s` of `α` that is well-ordered by the `<` relation, if the set `s` is nonempty, then the greatest lower bound of the set (`sInf s`) is an element of the set `s`.
More concisely: If `α` is a type with a conditionally complete linear order and `s ≠∅` is a well-ordered subset of `α` with respect to `<`, then `sInf s ∈ s`.
|
csInf_le_csInf
theorem csInf_le_csInf :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s t : Set α},
BddBelow t → s.Nonempty → s ⊆ t → sInf t ≤ sInf s
The theorem `csInf_le_csInf` states that for any type `α` which has a conditionally complete lattice structure and for any two sets `s` and `t` of `α`, if `t` is bounded below and `s` is nonempty, and every element of `s` is also an element of `t` (i.e., `s` is a subset of `t`), then the infimum of `t` is less than or equal to the infimum of `s`. This theorem is a property related to order theory and lattice theory, specifically it is about infimums in the context of conditionally complete lattices.
More concisely: In a conditionally complete lattice, the infimum of a nonempty subset that is also a subset of a bounded-below set is less than or equal to the infimum of the larger set.
|
csInf_singleton
theorem csInf_singleton : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] (a : α), sInf {a} = a
This theorem states that the infimum (greatest lower bound) of a singleton set in any conditionally complete lattice is the single element of that set. Here, a conditionally complete lattice is a type `α` that has a greatest lower bound and least upper bound for every nonempty set that has an upper bound or a lower bound respectively. Essentially, if you have a set with just one element `a`, then the greatest lower bound of this set is `a` itself.
More concisely: In a conditionally complete lattice, the infimum of a singleton set is its unique element.
|
csInf_le_csSup
theorem csInf_le_csSup :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α},
BddBelow s → BddAbove s → s.Nonempty → sInf s ≤ sSup s
The theorem `csInf_le_csSup` states that for any set `s` of a type `α`, where `α` is a conditionally complete lattice, if `s` is bounded both below and above and is also nonempty, then the infimum (greatest lower bound) of `s` is less than or equal to the supremum (least upper bound) of `s`. This is a fundamental property of ordered sets in mathematics and ensures that the notions of infimum and supremum are consistent and well-defined.
More concisely: For any nonempty, bounded above and below set `s` in a conditionally complete lattice `α`, the infimum of `s` is less than or equal to the supremum of `s`.
|
WithTop.coe_iInf
theorem WithTop.coe_iInf :
∀ {α : Type u_1} {ι : Sort u_4} [inst : Nonempty ι] [inst : InfSet α] (f : ι → α), ↑(⨅ i, f i) = ⨅ i, ↑(f i) := by
sorry
This theorem states that for any type `α`, any sort `ι`, given that `ι` is nonempty and `α` has an infimum set structure, for any function `f` from `ι` to `α`, the infimum of the co-domain of `f` when considered in the "WithTop" extension of `α` is equal to the "WithTop" extension of the infimum of the co-domain of `f`. In simpler terms, it establishes that taking the infimum then embedding into the "WithTop" extension is the same as embedding each element into the "WithTop" extension then taking the infimum.
More concisely: For any type `α` with an infimum set structure and nonempty sort `ι`, the infimum of the image of a function from `ι` to `α` in the "WithTop" extension of `α` equals the "WithTop" extension of the infimum of the function's image.
|
ciSup_mem_iInter_Icc_of_antitone_Icc
theorem ciSup_mem_iInter_Icc_of_antitone_Icc :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst_1 : SemilatticeSup β] {f g : β → α},
(Antitone fun n => Set.Icc (f n) (g n)) → (∀ (n : β), f n ≤ g n) → ⨆ n, f n ∈ ⋂ n, Set.Icc (f n) (g n)
The theorem `ciSup_mem_iInter_Icc_of_antitone_Icc` states that, given a conditionally complete lattice `α` and a `β` that is a semilattice with a supremum operation, if we have two functions `f` and `g` from `β` to `α` such that for every `n` in `β`, the closed interval `[f(n), g(n)]` forms an antitone sequence (i.e., if `a ≤ b` then the interval `[g(b), f(b)]` is a subset of `[g(a), f(a)]`), and `f(n)` is always less than or equal to `g(n)`, then the supremum of `f` over all `n` in `β` is contained in the intersection of all the intervals `[f(n), g(n)]`. In simpler terms, it says that in such a descending sequence of closed intervals, the supremum of the lower bounds lies in all the intervals.
More concisely: If `α` is a conditionally complete lattice and `β` is a semilattice with a supremum operation, given antitone functions `f` and `g` from `β` to `α` with `f(n) ≤ g(n)` for all `n` in `β`, then the supremum of `f` is contained in the intersection of all the intervals `[f(n), g(n)]`.
|
ciInf_le
theorem ciInf_le :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {f : ι → α},
BddBelow (Set.range f) → ∀ (c : ι), iInf f ≤ f c
This theorem states that for any type `α` with a Conditionally Complete Lattice structure, and any function `f` from an arbitrary type `ι` to `α`, if the range of the function `f` is bounded below, then the 'indexed infimum' (i.e., the greatest lower bound) of the function `f` is less than or equal to the value of the function at any point `c` in its domain. In mathematical terms, if `f : ι → α` and the set `{f(x) | x ∈ ι}` has a lower bound, then for any `c` in `ι`, we have `inf {f(x) | x ∈ ι} ≤ f(c)`.
More concisely: For any function `f : ι → α` with domain `ι` and type `α` having a Conditionally Complete Lattice structure, if the range of `f` has an infimum then `inf (range f) ≤ f(c)` for any `c` in `ι`.
|
Monotone.le_csSup_image
theorem Monotone.le_csSup_image :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : ConditionallyCompleteLattice β] {f : α → β},
Monotone f → ∀ {s : Set α} {c : α}, c ∈ s → BddAbove s → f c ≤ sSup (f '' s)
The theorem `Monotone.le_csSup_image` states that for any types `α` and `β`, where `α` has a preorder and `β` has a conditionally complete lattice structure, if there is a function `f` from `α` to `β` that is monotone, then for any set `s` of type `α` and any element `c` in `s`, if `s` is bounded above, then the image of `c` under `f` is less than or equal to the supremum of the image of `s` under `f`. In simpler terms, if a function is increasing and applied to a set that has an upper bound, then the value of the function at any point in the set is not greater than the maximum value the function takes on the set.
More concisely: For any monotonic function from a preordered type to a conditionally complete lattice, the image of any element in a bounded subset is less than or equal to the supremum of the images of that subset.
|
csSup_eq_of_forall_le_of_forall_lt_exists_gt
theorem csSup_eq_of_forall_le_of_forall_lt_exists_gt :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {b : α},
s.Nonempty → (∀ a ∈ s, a ≤ b) → (∀ w < b, ∃ a ∈ s, w < a) → sSup s = b
This theorem, `csSup_eq_of_forall_le_of_forall_lt_exists_gt`, states that for any set `s` of elements of a conditionally complete lattice `α`, and any element `b` from `α`, if `s` is nonempty, every element `a` in `s` is less than or equal to `b`, and for every element `w` less than `b`, there exists an element `a` in `s` that is greater than `w`, then `b` is the supremum of `s`. This can be used as an introduction rule to prove that `b` is the supremum of `s`. A similar version of this theorem exists for complete lattices.
More concisely: If `s` is a nonempty subset of a conditionally complete lattice `α` such that every element in `s` is less than or equal to every element `b` in `α` with `w < b` implying the existence of an element `a` in `s` with `w < a`, then `b` is the supremum of `s`.
|
csInf_le'
theorem csInf_le' :
∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α}, a ∈ s → sInf s ≤ a
The theorem `csInf_le'` states that for any type `α` that has an instance of `ConditionallyCompleteLinearOrderBot`, for any set `s` of type `α`, and for any element `a` of type `α`, if `a` is an element of the set `s`, then the greatest lower bound (infimum) of the set `s`, denoted as `sInf s`, is less than or equal to the element `a`. This theorem is a fundamental property in order theory, ensuring that the infimum of a set does not exceed any element of the set itself.
More concisely: For any set `s` in a type `α` with a `ConditionallyCompleteLinearOrderBot`, if an element `a` is in `s`, then `inf s ≤ a`.
|
WithTop.isGLB_sInf'
theorem WithTop.isGLB_sInf' :
∀ {β : Type u_5} [inst : ConditionallyCompleteLattice β] {s : Set (WithTop β)}, BddBelow s → IsGLB s (sInf s) := by
sorry
The theorem `WithTop.isGLB_sInf'` states that for any type `β` that forms a conditionally complete lattice, and for any set `s` of values within the type `β` with an attached top (`WithTop β`), if the set `s` is bounded below (i.e., there exists a lower bound for the elements in the set `s`), then the infimum (`sInf`) of the set `s` is its greatest lower bound. This essentially means the `sInf` is the greatest value that is less than or equal to all elements in the set `s` for such a conditionally complete lattice with a top.
More concisely: For any conditionally complete lattice `β` with a top element, if a set `s` in `β` has a bottom element, then the infimum of `s` is equal to its greatest lower bound.
|
le_csSup
theorem le_csSup :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α}, BddAbove s → a ∈ s → a ≤ sSup s := by
sorry
The theorem `le_csSup` states that for any type `α` which is a Conditionally Complete Lattice, any set `s` of type `α`, and any element `a` of type `α`, if the set `s` is bounded above (i.e., has an upper bound) and the element `a` is a member of the set `s`, then `a` is less than or equal to the supremum of the set `s`. Here, supremum (denoted as `sSup`) is the least upper bound of the set `s`.
More concisely: If `α` is a Conditionally Complete Lattice, `s` is a bounded above subset of `α`, and `a` is an element of `s`, then `a ≤ sSup`.
|
csInf_image2_eq_csInf_csInf
theorem csInf_image2_eq_csInf_csInf :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α]
[inst_1 : ConditionallyCompleteLattice β] [inst_2 : ConditionallyCompleteLattice γ] {s : Set α} {t : Set β}
{u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β},
(∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)) →
(∀ (a : α), GaloisConnection (l₂ a) (u a)) →
s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sInf (Set.image2 u s t) = u (sInf s) (sInf t)
This theorem states that for any three types `α`, `β`, and `γ` that are conditionally complete lattices, and for any sets `s` and `t` of types `α` and `β` respectively, along with a binary function `u : α → β → γ` and two Galois connections `l₁ : β → γ → α` and `l₂ : α → γ → β` (where the Galois connection for `l₁` is a function of `b` that has its order reversed by `u`, and similarly, the Galois connection for `l₂` is a function of `a` that has its order reversed by `u`), if `s` and `t` are nonempty and bounded below, then the infimum (greatest lower bound) of the image of the binary function `u` over sets `s` and `t` is equal to the value of the function `u` at the infimum of `s` and the infimum of `t`. This relates the infimum of a function's image over a Cartesian product of sets to the function's value at the Cartesian product of the infimums of those sets.
More concisely: Given three conditionally complete lattices `α`, `β`, `γ`, sets `s ≠∅` in `α`, `t ≠∅` in `β`, a binary function `u : α → β → γ`, and Galois connections `l₁ : β → γ → α` and `l₂ : α → γ → β` with reversed orders under `u`, if `inf s` and `inf t` exist, then `inf (map (λ x, λ y, u x y) s t) = u (inf s) (inf t)`.
|
Monotone.ciSup_mem_iInter_Icc_of_antitone
theorem Monotone.ciSup_mem_iInter_Icc_of_antitone :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst_1 : SemilatticeSup β] {f g : β → α},
Monotone f → Antitone g → f ≤ g → ⨆ n, f n ∈ ⋂ n, Set.Icc (f n) (g n)
**Nested Intervals Lemma**: For all `n`, consider a pair of sequences `f` and `g`, where `f` is monotone (i.e., `f` is a sequence that never decreases), `g` is antitone (i.e., `g` is a sequence that never increases), and every term of `f` is less than or equal to the corresponding term of `g`. Then the supremum of the `f` sequence (i.e., its least upper bound, represented as `⨆ n, f n`) lies within the intersection of all closed intervals `[f n, g n]` (i.e., the set of all values that are greater than or equal to `f n` and less than or equal to `g n` for all `n`).
More concisely: If `f` is a monotone increasing sequence with terms less than or equal to the corresponding terms of the antitone sequence `g`, then the supremum of `f` lies within the interval determined by `f` and `g`, i.e., `⋃ n, [f n, g n]`.
|
WithTop.sInf_empty
theorem WithTop.sInf_empty : ∀ {α : Type u_5} [inst : InfSet α], sInf ∅ = ⊤
This theorem states that for any type `α` where an infimum (greatest lower bound) of a set can be defined, the infimum of an empty set is the greatest element in the partially ordered set of elements extended with a top element (`WithTop`). In other words, in the extended set `WithTop α`, the infimum of an empty set is always the top element (`⊤`). This aligns with the standard mathematical convention where the infimum of an empty set in a set extended with a top element is the top element itself.
More concisely: In any partially ordered type `α` with a top element `⊤`, the infimum of an empty set equals `⊤`.
|
Monotone.csSup_image_le
theorem Monotone.csSup_image_le :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : ConditionallyCompleteLattice β] {f : α → β},
Monotone f → ∀ {s : Set α}, s.Nonempty → ∀ {B : α}, B ∈ upperBounds s → sSup (f '' s) ≤ f B
The theorem `Monotone.csSup_image_le` states that given a preordered set of type `α`, a conditionally complete lattice of type `β`, a function `f` from `α` to `β` that is monotone, a nonempty set `s` of type `α`, and an element `B` of type `α` that is an upper bound for the set `s`, the supremum of the image of `s` under `f`, if it exists, is less than or equal to `f(B)`. In other words, if a function is monotone, its supremum (the least upper bound) over the image of a nonempty set is less than or equal to the value of the function at any upper bound of the original set.
More concisely: If `f` is a monotone function from a preordered set `α` to a conditionally complete lattice `β`, and `s ≠ ∅` is a subset of `α` with an upper bound `B` in `α`, then the image of `s` under `f` has a supremum in `β` that is less than or equal to `f(B)`.
|
ConditionallyCompleteLattice.csInf_le
theorem ConditionallyCompleteLattice.csInf_le :
∀ {α : Type u_5} [self : ConditionallyCompleteLattice α] (s : Set α) (a : α), BddBelow s → a ∈ s → sInf s ≤ a := by
sorry
This theorem states that for any type `α` that has the structure of a Conditionally Complete Lattice, given a set `s` of type `α` and an element `a` of type `α`, if `s` is bounded below (`BddBelow s`), and `a` is an element of `s` (`a ∈ s`), then the infimum of `s` (denoted by `sInf s`) is less than or equal to `a`. In other words, for any element `a` in a set `s` that has a lower bound, the least element of `s` is not greater than `a`.
More concisely: For any conditionally complete lattice `α`, if `s` is a bounded below set in `α` and `a` is a member of `s`, then `inf s ≤ a`.
|
subset_Icc_csInf_csSup
theorem subset_Icc_csInf_csSup :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α},
BddBelow s → BddAbove s → s ⊆ Set.Icc (sInf s) (sSup s)
The theorem `subset_Icc_csInf_csSup` states that for any set `s` of elements of some type `α`, where `α` forms a conditionally complete lattice, if `s` is both bounded from below (i.e., there exists a lower bound for `s`) and from above (i.e., there exists an upper bound for `s`), then `s` is a subset of the closed interval between the infimum (`sInf s`) and the supremum (`sSup s`) of `s`. In other words, all elements of `s` are greater than or equal to the infimum of `s` and less than or equal to the supremum of `s`.
More concisely: If a set `s` of a conditionally complete lattice `α` has both a lower bound and an upper bound, then `s` is contained in the closed interval between the infimum and supremum of `s`.
|
csSup_le
theorem csSup_le :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α},
s.Nonempty → (∀ b ∈ s, b ≤ a) → sSup s ≤ a
The theorem `csSup_le` states that for any type `α` that is a conditionally complete lattice, any non-empty set `s` of type `α`, and any element `a` of type `α`, if every element `b` in `s` is less than or equal to `a`, then the supremum (or least upper bound) of `s` is less than or equal to `a`. In other words, if `a` is an upper bound of a non-empty set in a conditionally complete lattice, then it is at least as large as the supremum of that set.
More concisely: If `α` is a conditionally complete lattice and `s` is a non-empty subset of `α` with `a` as an upper bound, then `sup s ≤ a`.
|
OrderIso.map_csSup'
theorem OrderIso.map_csSup' :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst_1 : ConditionallyCompleteLattice β]
(e : α ≃o β) {s : Set α}, s.Nonempty → BddAbove s → e (sSup s) = sSup (⇑e '' s)
This theorem states that for any two types `α` and `β` that are both conditionally complete lattices, an order isomorphism `e` from `α` to `β`, and a non-empty set `s` of type `α` that is bounded above, the supremum of `s` under the isomorphism `e` is equal to the supremum of the image of `s` under `e`. In other words, applying an order isomorphism preserves the supremum of a set.
More concisely: For any conditionally complete lattices `α` and `β`, order isomorphism `e : α ≃ β`, and non-empty bounded-above set `s : α`, the supremum of `s` under `e` equals the supremum of `e(s)` in `β`.
|
csInf_lt_of_lt
theorem csInf_lt_of_lt :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a b : α},
BddBelow s → a ∈ s → a < b → sInf s < b
The theorem `csInf_lt_of_lt` states that for any type `α` that is a conditionally complete lattice, any set `s` of type `α`, and any two elements `a` and `b` of type `α`, if `s` is bounded below, and `a` is an element of `s` such that `a` is less than `b`, then the infimum (greatest lower bound) of the set `s` is less than `b`. It's important to note that the conditions for this statement to hold are not symmetrical: one direction requires the set to be bounded below, while the other requires the set to be nonempty and have a linear order. This is contrasted with the case for complete lattices, where the conditions are the same for both directions.
More concisely: If `α` is a conditionally complete lattice, `s` is a nonempty, bounded below set in `α`, and `a` is in `s` with `a < b`, then the infimum of `s` is less than `b`.
|
csSup_le'
theorem csSup_le' :
∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α},
a ∈ upperBounds s → sSup s ≤ a
This theorem, `csSup_le'`, states that for any type `α` that has a structure of a conditionally complete linear order with a least element (expressed as `ConditionallyCompleteLinearOrderBot α`), for any set `s` of elements of type `α`, and for any element `a` of type `α`, if `a` is in the set of upper bounds of `s` (expressed as `a ∈ upperBounds s`), then the supremum of `s` (expressed as `sSup s`) is less than or equal to `a`. In simpler terms, it says that the supremum of a set is always less than or equal to any of the set's upper bounds.
More concisely: For any conditionally complete linear order `α` with a least element, and any set `s` of elements from `α` with upper bound `a`, the supremum of `s` is less than or equal to `a`.
|
ConditionallyCompleteLinearOrder.csInf_of_not_bddBelow
theorem ConditionallyCompleteLinearOrder.csInf_of_not_bddBelow :
∀ {α : Type u_5} [self : ConditionallyCompleteLinearOrder α] (s : Set α), ¬BddBelow s → sInf s = sInf ∅
This theorem states that if a set, in the context of a conditionally complete linear order, is not bounded below, then the greatest lower bound (infimum) of this set is, by convention, the greatest lower bound of the empty set. Here, "not bounded below" means that there is no element that serves as a lower limit for all elements of the set.
More concisely: In a conditionally complete linear order, if a set has no lower bound, then its infimum equals the infimum of the empty set.
|
isGLB_csInf
theorem isGLB_csInf :
∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α}, s.Nonempty → BddBelow s → IsGLB s (sInf s)
The theorem `isGLB_csInf` states that, for any given set `s` of a certain type `α`, if `s` is non-empty (`Set.Nonempty s`) and bounded below (`BddBelow s`), then the infimum (`sInf s`) of `s` is indeed a greatest lower bound of `s` (`IsGLB s`). Here, `α` is assumed to be a conditionally complete lattice, a mathematical structure with order relation where every nonempty, bounded below subset has an infimum. This theorem confirms that the infimum operation always results in a valid greatest lower bound for any non-empty and bounded below set in a conditionally complete lattice.
More concisely: In a conditionally complete lattice, the infimum of any non-empty and bounded below set is its greatest lower bound.
|
WithTop.coe_iSup
theorem WithTop.coe_iSup :
∀ {α : Type u_1} {ι : Sort u_4} [inst : Preorder α] [inst_1 : SupSet α] (f : ι → α),
BddAbove (Set.range f) → ↑(⨆ i, f i) = ⨆ i, ↑(f i)
This theorem states that for any type `α` with a preorder and superset structure, and any function `f` from some arbitrary type `ι` to `α`, if the range of `f` is bounded above, then the supremum (least upper bound) of the co-domain of `f` when mapped to the extended non-negative real line (with the possibility of positive infinity), is equal to the supremum of the image of `f` under the same mapping. In other words, taking the supremum of `f` before or after applying the function does not change the result, provided that the range of `f` is bounded above.
More concisely: For any function `f` from a type `ι` to a type `α` with a preorder and superset structure, if `f` has a bounded above range, then the supremum of `f`'s image equals the supremum of its range when mapped to the extended non-negative real line.
|
ciSup_le_iff'
theorem ciSup_le_iff' :
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] {f : ι → α},
BddAbove (Set.range f) → ∀ {a : α}, ⨆ i, f i ≤ a ↔ ∀ (i : ι), f i ≤ a
This theorem states that for all types `α` and `ι` where `α` has an instance of `ConditionallyCompleteLinearOrderBot`, and for a function `f` mapping values of `ι` to `α`, if the set of all values in the range of `f` is bounded above, then for any value `a` in `α`, the supremum of `f` over all `ι` is less than or equal to `a` if and only if `f(i)` is less than or equal to `a` for all `i` in `ι`. In other words, if we have a bound for the range of a function, this bound is bigger than or equal to the supremum of the function if and only if it is bigger than or equal to all the values of the function. Here, `ConditionallyCompleteLinearOrderBot` means that `α` is a conditionally complete linear order with a bottom element.
More concisely: If `α` is a conditionally complete linear order with a bottom element, and `f:` `ι` → `α` has a bounded range above some element `a` in `α`, then `sup(f) ≤ a` if and only if `f(i) ≤ a` for all `i` in `ι`.
|
OrderIso.map_csInf'
theorem OrderIso.map_csInf' :
∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst_1 : ConditionallyCompleteLattice β]
(e : α ≃o β) {s : Set α}, s.Nonempty → BddBelow s → e (sInf s) = sInf (⇑e '' s)
The theorem `OrderIso.map_csInf'` states that for any two types `α` and `β`, each equipped with a conditionally complete lattice structure, and an order isomorphism `e` from `α` to `β`, if `s` is a nonempty set in `α` that is bounded below, then the image of the infimum (greatest lower bound) of `s` under `e` is equal to the infimum of the image of `s` under `e`. In other words, the order isomorphism `e` preserves the infimum operation from `α` to `β` for sets that are nonempty and have a lower bound.
More concisely: For order isomorphisms between conditionally complete lattices, the image of the infimum of a nonempty, bounded-below set under the isomorphism is equal to the infimum of the image of that set.
|