eq_of_mabs_div_le_all — Mathlib

English

In a densely ordered group, if for all ε > 1 we have |a/b|_m ≤ ε, then a = b.

Русский

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

LaTeX

$$\forall \varepsilon>1, |a/b|_m \le \varepsilon \implies a=b \quad (\text{densely ordered})$$

Lean4

@[to_additive]
theorem eq_of_mabs_div_le_all [DenselyOrdered G] {x y : G} (h : ∀ ε > 1, |x / y|ₘ ≤ ε) : x = y :=
  eq_of_mabs_div_le_one <| forall_gt_imp_ge_iff_le_of_dense.mp h

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