mabs_div_le_one — Mathlib

English

Same as above for a densely ordered group; if for all ε>1, |a/b|_m ≤ ε, then a=b.

Русский

То же самое в плотно упорядоченной группе: если для всех ε>1 выполняется |a/b|ₘ ≤ ε, то a=b.

LaTeX

$$\forall \varepsilon>1, |a/b|_m \le \varepsilon \implies a=b \quad (плотный порядок)$$

Lean4

@[to_additive]
theorem mabs_div_le_one : |a / b|ₘ ≤ 1 ↔ a = b :=
  ⟨eq_of_mabs_div_le_one, by rintro rfl; rw [div_self', mabs_one]⟩

Похожие утверждения