English
For distinct x,y, the distance between them is contained in the lower bound of the Einfsep of the pair; in particular the minimum of edist(x,y) and edist(y,x) is at most einfsep({x,y}).
Русский
Для различных x,y истинно, что расстояние между ними не превосходит einfsep({x,y}); точнее, min{edist(x,y), edist(y,x)} ≤ einfsep({x,y}).
LaTeX
$$$ \min\bigl( \operatorname{edist}(x,y), \operatorname{edist}(y,x) \bigr) \le \operatorname{einfsep}({x,y}) $$$
Lean4
theorem le_einfsep_pair : edist x y ⊓ edist y x ≤ ({ x, y } : Set α).einfsep :=
by
simp_rw [le_einfsep_iff, inf_le_iff, mem_insert_iff, mem_singleton_iff]
rintro a (rfl | rfl) b (rfl | rfl) hab <;> (try simp only [le_refl, true_or, or_true]) <;> contradiction
