isClosed_isNowhereDense_iff_compl

Mathlib.Topology.GDelta.Basic

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

← MathLib Explorer

English

The empty set is meagre.

Русский

Пусть пустое множество — мезгрей.

LaTeX

$$IsMeagre(∅)$$

Lean4

/-- A set `s` is closed and nowhere dense iff its complement `sᶜ` is open and dense. -/
theorem isClosed_isNowhereDense_iff_compl {s : Set X} : IsClosed s ∧ IsNowhereDense s ↔ IsOpen sᶜ ∧ Dense sᶜ := by
  rw [and_congr_right IsClosed.isNowhereDense_iff, isOpen_compl_iff, interior_eq_empty_iff_dense_compl]

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

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

Разделы

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

Аффилиация

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