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.