residual_of_dense_open

Mathlib.Topology.GDelta.Basic

URI: https://scilib.ai/kg/mathlib#residual_of_dense_open

← MathLib Explorer

English

Dense open sets are residual.

Русский

Плотные открытые множества — резидуальные.

LaTeX

$$$IsOpen(s)\\land Dense(s)\\Rightarrow s\\in residual(X)$$$

Lean4

/-- Dense open sets are residual. -/
theorem residual_of_dense_open {s : Set X} (ho : IsOpen s) (hd : Dense s) : s ∈ residual X :=
  CountableGenerateSets.basic ⟨ho, hd⟩

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

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

Разделы

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

Аффилиация

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