einfsep_pair_eq_inf — Mathlib

English

For distinct x,y, einfsep({x,y}) equals edist(x,y) ⊓ edist(y,x) (the two distances).

Русский

Для различных x,y einfsep({x,y}) равно edist(x,y) ⊓ edist(y,x) (мин расстояний).

LaTeX

$$$ \operatorname{einfsep}({x,y}) = \operatorname{edist}(x,y) \sqcap \operatorname{edist}(y,x) $$$

Lean4

theorem einfsep_pair_eq_inf (hxy : x ≠ y) : ({ x, y } : Set α).einfsep = edist x y ⊓ edist y x :=
  le_antisymm (le_inf (einfsep_pair_le_left hxy) (einfsep_pair_le_right hxy)) le_einfsep_pair

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