csSup_mem_of_not_isSuccLimit
theorem csSup_mem_of_not_isSuccLimit :
∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α},
s.Nonempty → BddAbove s → ¬Order.IsSuccLimit (sSup s) → sSup s ∈ s
This theorem states that for any non-empty set `s` of elements of type `α`, where `α` is a conditionally complete linear order, if `s` is bounded above and the supremum of `s` (denoted as `sSup s`) is not a successor limit, then `sSup s` is an element of `s`.
In other words, the least upper bound or supremum of a non-empty set that has an upper bound and is not a successor limit, is guaranteed to be an element of the set itself.
More concisely: If `s` is a non-empty, bounded above subset of a conditionally complete linear order `α` without a successor limit supreme, then `sSup s` is an element of `s`.
|
csSup_mem_of_not_isSuccLimit'
theorem csSup_mem_of_not_isSuccLimit' :
∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] {s : Set α},
BddAbove s → ¬Order.IsSuccLimit (sSup s) → sSup s ∈ s
This theorem states that for any type `α` that has a structure of a conditionally complete linear order with a bottom element, and for any set `s` of type `α`, if the set `s` is bounded above and the supremum of `s` (denoted by `sSup s`) is not a successor limit, then the supremum of `s` is an element of `s`. In other words, if `s` has an upper bound and there is no element in `s` that is smaller than and incomparable with its supremum, then the supremum is contained in the set `s` itself.
More concisely: If `s` is a bounded above subset of a conditionally complete linear order `α` with a bottom element, and `sSup s` is not a successor limit, then `sSup s` is an element of `s`.
|
exists_eq_ciSup_of_not_isSuccLimit'
theorem exists_eq_ciSup_of_not_isSuccLimit' :
∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] {f : ι → α},
BddAbove (Set.range f) → ¬Order.IsSuccLimit (⨆ i, f i) → ∃ i, f i = ⨆ i, f i
This theorem, `exists_eq_ciSup_of_not_isSuccLimit'`, states that for any type `ι` and a type `α` that is a `ConditionallyCompleteLinearOrderBot` (basically, a type that is a complete linear order with a least element), given a function `f` mapping from `ι` to `α`, if the range of `f` is bounded above and the supremum (the least upper bound) of `f(i)` for all `i` is not a successor limit (meaning there is no value that is lesser than but uncomparable to the supremum), then there exists an `i` such that `f(i)` is equal to the supremum of `f(i)` for all `i`.
In simpler terms, if the set of all outputs of a function is bounded from above and the upper bound isn't a successor limit, then there must be a point in the function's domain that maps to this upper bound.
More concisely: If `ι` is a type with a least element and `α` is a conditionally complete linear order, `f : ι → α` is a function with a bounded above range, and the supremum of `f` is not a successor limit, then there exists an `i` such that `f(i)` equals the supremum of `f`.
|