Commit 2026-01-23 10:44 31295c01

View on Github →

feat(Analysis/Real/Hyperreal): more lemmas on ω and ε (#33649) I've moved these around a bit, so as to ensure the lemmas about each constant are next to each other.

Estimated changes

Modified Mathlib/Algebra/Order/AddGroupWithTop.lean

added theorem LinearOrderedAddCommGroupWithTop.neg_pos

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

added theorem ArchimedeanClass.lt_of_neg_of_archimedean

added theorem ArchimedeanClass.lt_of_pos_of_archimedean

Modified Mathlib/Analysis/Real/Hyperreal.lean

added theorem Hyperreal.abs_omega

added theorem Hyperreal.archimdeanClassMk_coe

added theorem Hyperreal.archimedeanClassMk_coe_nonneg

added theorem Hyperreal.archimedeanClassMk_epsilon_pos

added theorem Hyperreal.archimedeanClassMk_omega_neg

added def Hyperreal.coeRingHom

added theorem Hyperreal.coe_lt_omega

added def Hyperreal.epsilon

added theorem Hyperreal.epsilon_lt_of_neg

added theorem Hyperreal.epsilon_lt_of_pos

deleted theorem Hyperreal.epsilon_lt_pos

added def Hyperreal.ofReal

added def Hyperreal.ofSeq

added def Hyperreal.omega

added def Hyperreal.st

added theorem Hyperreal.stdPart_coe

added theorem Hyperreal.stdPart_epsilon

added theorem Hyperreal.stdPart_omega