Commit 2025-02-19 20:44 5f3459dd

View on Github →

feat: (∀ ε > 0, |x - y| < ε) → x = y (#22088)

Estimated changes

Modified Mathlib/Algebra/Order/Group/Abs.lean

added theorem eq_of_abs_sub_le_all

added theorem eq_of_abs_sub_lt_all