einfsep_eq_top_iff

Mathlib.Topology.MetricSpace.Infsep

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

English

Einfsep equals ∞ if and only if the set is subsingleton.

Русский

einfsep(s) = ∞ эквивалентно тому, что s является subsingleton.

LaTeX

$$$ \operatorname{einfsep}(s) = \infty \iff s \text{ is a subsingleton} $$$

Lean4

theorem einfsep_eq_top_iff : s.einfsep = ∞ ↔ s.Subsingleton :=
  ⟨subsingleton_of_einfsep_eq_top, Subsingleton.einfsep⟩

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

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

Разделы

Аффилиация

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