The real numbers are an Archimedean floor ring, and a conditionally complete linear order. #
Equations
Equations
- Real.instSupSet = { sSup := fun (s : Set ℝ) => if h : s.Nonempty ∧ BddAbove s then Classical.choose ⋯ else 0 }
@[deprecated isGLB_sInf (since := "2024-10-02")]
Alias of isGLB_sInf
.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[simp]
As ⨆ i, f i = 0
when the domain of the real-valued function f
is empty,
it suffices to show that all values of f
are nonpositive to show that ⨆ i, f i ≤ 0
.
As ⨅ i, f i = 0
when the real-valued function f
is unbounded below,
it suffices to show that f
takes a nonpositive value to show that 0 ≤ ⨅ i, f i
.
As ⨅ i, f i = 0
when the domain of the real-valued function f
is empty or unbounded below,
it suffices to show that all values of f
are nonpositive to show that 0 ≤ ⨅ i, f i
.