Commit 2024-11-18 18:16 2ff73d59

feat(Mathlib/Algebra/Order): add equivalent conditions to a ≤ b (#19166) Two theorems that give equivalent conditions to a ≤ b in terms of ε-approximation.

• Generalize a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε (le_iff_forall_one_lt_le_mul) to monoids.
• Add (hb : 0 ≤ b) : a ≤ b ↔ ∀ ε, 1 < ε → a ≤ b * ε for linearly ordered semifields. the proofs were suggested by @fpvandoorn in this thread motivation: I will need them in the proof of regularity of rieszContent, that will be defined after #18775