infsep_pair_le_toReal_inf — Mathlib

English

For two points x,y, the infsep of {x,y} is bounded by the real representation of their distance.

Русский

Для пары точек x,y инфsep множества {x,y} не превышает преобразование edist x y в действительное число.

LaTeX

$$$ ({ x,y } : Set α).infsep \le (edist x y \sqcap edist y x).toReal $$$

Lean4

theorem infsep_pair_le_toReal_inf (hxy : x ≠ y) : ({ x, y } : Set α).infsep ≤ (edist x y ⊓ edist y x).toReal :=
  by
  simp_rw [infsep, einfsep_pair_eq_inf hxy]
  simp

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