einfsep_pair_le_right

Mathlib.Topology.MetricSpace.Infsep

URI: https://scilib.ai/kg/mathlib#Set.einfsep_pair_le_right

English

If x ≠ y, then einfsep({x,y}) ≤ edist(y,x).

Русский

Если x ≠ y, то einfsep({x,y}) ≤ edist(y,x).

LaTeX

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

Lean4

theorem einfsep_pair_le_right (hxy : x ≠ y) : ({ x, y } : Set α).einfsep ≤ edist y x := by rw [pair_comm];
  exact einfsep_pair_le_left hxy.symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru