einfsep_ne_top

Mathlib.Topology.MetricSpace.Infsep

URI: https://scilib.ai/kg/mathlib#Set.Nontrivial.einfsep_ne_top

English

If s is nontrivial, then einfsep(s) is not equal to the top (infinity).

Русский

Если s не тривиально, то einfsep(s) не равно топ (бесконечности).

LaTeX

$$$ s.Nontrivial \Rightarrow s.einfsep \neq \infty $$$

Lean4

theorem einfsep_ne_top (hs : s.Nontrivial) : s.einfsep ≠ ∞ :=
  by
  contrapose! hs
  exact subsingleton_of_einfsep_eq_top hs

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

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

Разделы

Аффилиация

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