eq_of_forall_edist_le — Mathlib

English

If for all ε>0 we have edist x y ≤ ε, then x = y.

Русский

Если для всех ε>0 выполняется edist x y ≤ ε, то x = y.

LaTeX

$$$(\\forall \\varepsilon>0, \\; \\mathrm{edist}(x,y) \\le \\varepsilon) \\Rightarrow x=y$$$

Lean4

/-- Two points coincide if their distance is `< ε` for all positive ε -/
theorem eq_of_forall_edist_le {x y : γ} (h : ∀ ε > 0, edist x y ≤ ε) : x = y :=
  eq_of_edist_eq_zero (eq_of_le_of_forall_lt_imp_le_of_dense bot_le h)

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