einfsep_pair_le_left

Mathlib.Topology.MetricSpace.Infsep

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem einfsep_pair_le_left (hxy : x ≠ y) : ({ x, y } : Set α).einfsep ≤ edist x y :=
  einfsep_le_edist_of_mem (mem_insert _ _) (mem_insert_of_mem _ (mem_singleton _)) hxy

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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