infsep_pair_eq_toReal — Mathlib

English

For distinct x,y, the infsep of {x,y} equals toReal(edist x y).

Русский

Для различий x,y инфsep пары {x,y} равен toReal(edist x y).

LaTeX

$$$ ({ x,y } : Set α).infsep = (edist x y).toReal $$$

Lean4

theorem infsep_pair_eq_toReal : ({ x, y } : Set α).infsep = (edist x y).toReal :=
  by
  by_cases hxy : x = y
  · rw [hxy]
    simp only [infsep_singleton, pair_eq_singleton, edist_self, ENNReal.toReal_zero]
  · rw [infsep, einfsep_pair hxy]

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