einfsep_empty

Mathlib.Topology.MetricSpace.Infsep

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

English

The non-top property: s.einfsep ≠ ∞ iff there exist x,y ∈ s with x ≠ y and edist x y ≠ ∞.

Русский

Неравенство s.einfsep ≠ ∞ эквивалентно существованию x,y ∈ s с x ≠ y и edist x y ≠ ∞.

LaTeX

$$$s.einfsep \neq \infty \iff \exists x \in s, \exists y \in s, x \neq y \land edist x y \neq \infty$$$

Lean4

@[simp]
theorem einfsep_empty : (∅ : Set α).einfsep = ∞ :=
  subsingleton_empty.einfsep

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

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

Разделы

Аффилиация

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