subset_of_closed_isNowhereDense — Mathlib

English

A set s is closed and nowhere dense iff its complement sᶜ is open and dense.

Русский

Множество s замкнутое и нигде плотное тогда и только тогда, когда его дополнение открыто и плотное.

LaTeX

$$IsClosed s ∧ IsNowhereDense s ↔ IsOpen s^c ∧ Dense s^c$$

Lean4

/-- A nowhere dense set `s` is contained in a closed nowhere dense set (namely, its closure). -/
theorem subset_of_closed_isNowhereDense {s : Set X} (hs : IsNowhereDense s) :
    ∃ t : Set X, s ⊆ t ∧ IsNowhereDense t ∧ IsClosed t :=
  ⟨closure s, subset_closure, ⟨hs.closure, isClosed_closure⟩⟩

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