Commit 2026-01-02 14:04 e2a59516

View on Github →

feat: stdPart x = sSup {r | r < x} (#33007)

Estimated changes

Modified Mathlib/Algebra/Order/Archimedean/Class.lean

added theorem MulArchimedeanClass.min_le_mk_of_le_of_le

added theorem MulArchimedeanClass.mk_le_mk_of_mabs

Modified Mathlib/Algebra/Order/Ring/Archimedean.lean

added theorem ArchimedeanClass.exists_int_ge_of_mk_nonneg

added theorem ArchimedeanClass.exists_int_gt_of_mk_nonneg

added theorem ArchimedeanClass.exists_int_le_of_mk_nonneg

added theorem ArchimedeanClass.exists_int_lt_of_mk_nonneg

added theorem ArchimedeanClass.exists_nat_ge_of_mk_nonneg

added theorem ArchimedeanClass.exists_nat_gt_of_mk_nonneg

added theorem ArchimedeanClass.mk_nonneg_of_le_of_le_of_archimedean

Modified Mathlib/Algebra/Order/Ring/StandardPart.lean

added theorem ArchimedeanClass.stdPart_eq

added theorem ArchimedeanClass.stdPart_eq_sInf

added theorem ArchimedeanClass.stdPart_eq_sSup

Modified Mathlib/Data/Real/Archimedean.lean

added theorem Real.sInf_neg

added theorem Real.sSup_neg