einfsep_singleton

Mathlib.Topology.MetricSpace.Infsep

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

English

The einfsep of a singleton is infinite: einfsep({x}) = ∞.

Русский

Расширенная инфиминальная разделённость одинокого множества равна бесконечности.

LaTeX

$$$({x})\text{ is singleton} \Rightarrow ({x})\einfsep = \infty$$$

Lean4

@[simp]
theorem einfsep_singleton : ({ x } : Set α).einfsep = ∞ :=
  subsingleton_singleton.einfsep

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

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

Разделы

Аффилиация

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