disjoint_nhdsSet_cobounded

Mathlib.Topology.MetricSpace.Bounded

URI: https://scilib.ai/kg/mathlib#Metric.disjoint_nhdsSet_cobounded

← MathLib Explorer

English

If s is compact, then nhdsSet(s) is disjoint from cobounded α.

Русский

Если s компактно, то nhdsSet(s) дисjoint от cobounded α.

LaTeX

$$$\\\\forall s:\\\\text{Set} α, IsCompact(s) \\Rightarrow Disjoint(nhdsSet(s), cobounded(\\\\alpha)).$$$

Lean4

theorem disjoint_nhdsSet_cobounded {s : Set α} (hs : IsCompact s) : Disjoint (𝓝ˢ s) (cobounded α) :=
  hs.disjoint_nhdsSet_left.2 fun _ _ ↦ disjoint_nhds_cobounded _

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

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

Разделы

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

Аффилиация

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