empty_right

Mathlib.Topology.Separation.SeparatedNhds

URI: https://scilib.ai/kg/mathlib#SeparatedNhds.empty_right

← MathLib Explorer

English

The right-empty variant: SeparatedNhds s ∅ holds.

Русский

Версия с правой частью пустой: SeparatedNhds s ∅ выполняется.

LaTeX

$$$ \mathrm{SeparatedNhds}(s, \varnothing) $$$

Lean4

@[simp]
theorem empty_right (s : Set X) : SeparatedNhds s ∅ :=
  ⟨_, _, isOpen_univ, isOpen_empty, fun a _ => mem_univ a, Subset.rfl, disjoint_empty _⟩

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

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

Разделы

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

Аффилиация

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