Theorem ArchimedeanClass.mk_nonneg_of_le_of_le_of_archimedean

Modification history

2026-01-02 14:04
Mathlib/Algebra/Order/Ring/Archimedean.lean
feat: `stdPart x = sSup {r | r < x}` (#33007)
Added ArchimedeanClass.mk_nonneg_of_le_of_le_of_archimedeanView on Github →