Real.sInf_nonpos
theorem Real.sInf_nonpos : ∀ (S : Set ℝ), (∀ x ∈ S, x ≤ 0) → sInf S ≤ 0
This theorem, named `Real.sInf_nonpos`, states that for any set `S` of real numbers, if every element `x` in `S` is less than or equal to `0`, then the greatest lower bound (or infimum) of `S`, denoted by `sInf S`, is also less than or equal to `0`. In other words, if all elements of a set of real numbers are nonpositive, then its infimum is also nonpositive.
More concisely: If every real number in a set is nonpositive, then the infimum of the set is also nonpositive.
|
Real.sSup_nonpos
theorem Real.sSup_nonpos : ∀ (S : Set ℝ), (∀ x ∈ S, x ≤ 0) → sSup S ≤ 0
The theorem `Real.sSup_nonpos` states that for any set `S` of real numbers, if every element `x` in `S` is less than or equal to `0`, then the supremum (least upper bound) of `S` is also less than or equal to `0`. This is because `0` is the default value for the supremum of an empty set in the real numbers, so if all elements of `S` are bounded above by `0`, it follows that the supremum of `S` should not exceed `0`.
More concisely: If every element in a real number set S is non-positive, then the supremum of S is also non-positive.
|
Real.sInf_empty
theorem Real.sInf_empty : sInf ∅ = 0
This theorem states that the infimum (greatest lower bound) of an empty set in the domain of real numbers is zero. In other words, when we try to find the lowest value (infimum) in a set of real numbers, and the set is empty, we consider the infimum to be zero.
More concisely: The infimum of an empty set of real numbers is 0.
|
Real.iInf_nonneg
theorem Real.iInf_nonneg : ∀ {ι : Sort u_1} {f : ι → ℝ}, (∀ (i : ι), 0 ≤ f i) → 0 ≤ iInf f
The theorem `Real.iInf_nonneg` states that for any index type ι and any function `f` from ι to the real numbers, if every value of `f` at any index is greater than or equal to `0`, then the indexed infimum (or greatest lower bound) of `f`, denoted by `iInf f`, is also greater than or equal to `0`. This is because the default value for the supremum infimum `Real.sInf` of an empty set in real numbers is `0`.
More concisely: For any index type ι and real-valued function f from ι, if all values of f are non-negative, then the indexed infimum iInf(f) ≥ 0.
|
Real.iSup_of_isEmpty
theorem Real.iSup_of_isEmpty : ∀ {α : Sort u_1} [inst : IsEmpty α] (f : α → ℝ), ⨆ i, f i = 0
This theorem states that for any function `f` from an empty type `α` to the real numbers `ℝ`, the supremum (i.e., the least upper bound) of the image of `f` is zero. In other words, if you have a function mapping from an empty set to the real numbers, the largest value that function can achieve is zero.
More concisely: For any function from the empty type to the real numbers, the supremum of its image equals 0.
|
Real.sSup_nonneg
theorem Real.sSup_nonneg : ∀ (S : Set ℝ), (∀ x ∈ S, 0 ≤ x) → 0 ≤ sSup S
The theorem `Real.sSup_nonneg` asserts that for any set `S` of real numbers, if every element `x` in `S` satisfies the property that `x` is greater than or equal to 0 (denoted as `0 ≤ x`), then the supremum (`sSup`) of the set `S` is also greater than or equal to 0 (denoted as `0 ≤ sSup S`). Note that the supremum of a set is the least upper bound of that set, and in the context of this theorem, `0` is the default value for the supremum of an empty set or sets which are not bounded above.
More concisely: If every real number in a set is non-negative, then the supremum of the set is also non-negative.
|
Real.sSup_empty
theorem Real.sSup_empty : sSup ∅ = 0
This theorem states that the supremum (greatest value) of an empty set in the realm of real numbers is zero. The supremum, often denoted as sup or sSup in this context, is the least upper bound of a set. Since an empty set doesn't contain any elements, we conventionally define its supremum to be zero.
More concisely: The supremum of an empty set of real numbers is 0.
|
Real.sInf_of_not_bddBelow
theorem Real.sInf_of_not_bddBelow : ∀ {s : Set ℝ}, ¬BddBelow s → sInf s = 0
This theorem states that for any set of real numbers, if the set is not bounded below (i.e., it doesn't have a minimum value or a lower limit), then the greatest lower bound (infimum) of the set is zero. In other words, if a set of real numbers can extend indefinitely in the negative direction, then its infimum is zero.
More concisely: If a non-empty set of real numbers has no lowest element, then its infimum is 0.
|
Real.iSup_nonneg
theorem Real.iSup_nonneg : ∀ {ι : Sort u_1} {f : ι → ℝ}, (∀ (i : ι), 0 ≤ f i) → 0 ≤ ⨆ i, f i
This theorem states that for any index set `ι` and any function `f` from `ι` to the real numbers, if every value `f i` is nonnegative (that is, `0 ≤ f i` for all `i` in `ι`), then the supremum (least upper bound) of the set of all `f i` is also nonnegative. This is because `0` is the default value for supremum of empty set or sets which are not bounded above in real numbers.
More concisely: If `f:` `ι` -> **R** is a function such that `0 ≤ f i` for all `i` in `ι`, then `0 ≤ sup {f i | i ∈ ι}`.
|
Real.sSup_le
theorem Real.sSup_le : ∀ {S : Set ℝ} {a : ℝ}, (∀ x ∈ S, x ≤ a) → 0 ≤ a → sSup S ≤ a
The theorem `Real.sSup_le` states that for any set `S` of real numbers and any real number `a`, if every element `x` in `S` is less than or equal to `a` and `a` is nonnegative, then the supremum (`sSup`) of `S` is less than or equal to `a`. The supremum of a set in real numbers is the smallest real number that is greater than or equal to every number in the set. If the set is empty or does not have an upper bound, its supremum defaults to `0`. Hence, to show that the supremum of a set is bounded by a nonnegative number, it is enough to show that all elements of the set are bounded by this number.
More concisely: If `S` is a set of real numbers with every element less than or equal to non-negative `a`, then the supremum of `S` is less than or equal to `a`.
|
Real.sInf_nonneg
theorem Real.sInf_nonneg : ∀ (S : Set ℝ), (∀ x ∈ S, 0 ≤ x) → 0 ≤ sInf S
This theorem states that for any set `S` of real numbers, if every element `x` in `S` is greater than or equal to zero, then the greatest lower bound (infimum) of `S` is also greater than or equal to zero. The theorem uses the fact that 0 is the default value for the greatest lower bound of the empty set in its proof.
More concisely: If every element of a set `S` of real numbers is non-negative, then the infimum of `S` is also non-negative.
|
Real.sSup_of_not_bddAbove
theorem Real.sSup_of_not_bddAbove : ∀ {s : Set ℝ}, ¬BddAbove s → sSup s = 0
The theorem `Real.sSup_of_not_bddAbove` states that for any set `s` of real numbers, if `s` is not bounded above, then the supremum of `s` is equal to zero. This means if there is no real number that serves as an upper bound for all elements in the set `s`, then the least upper bound (or supremum) of this set is zero.
More concisely: If a set of real numbers has no upper bound, then its supremum equals 0.
|
Real.isLUB_sSup
theorem Real.isLUB_sSup : ∀ (S : Set ℝ), S.Nonempty → BddAbove S → IsLUB S (sSup S)
The theorem `Real.isLUB_sSup` states that for any given set `S` of real numbers, if `S` is not empty (`Set.Nonempty S`) and `S` is bounded above (`BddAbove S`), then the supremum of `S` (`sSup S`) is the least upper bound of `S`. In other words, for any non-empty set of real numbers that has an upper bound, the smallest value that is greater than or equal to every number in the set (supremum) is also the least upper bound of the set.
More concisely: For any non-empty, bounded above set of real numbers S, the supremum of S is the least upper bound of S.
|