closure — Mathlib

English

A nowhere dense set s is contained in a closed nowhere dense set (namely its closure).

Русский

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

LaTeX

$$∃ t : Set X, s ⊆ t ∧ IsNowhereDense t ∧ IsClosed t$$

Lean4

/-- If a set `s` is nowhere dense, so is its closure. -/
protected theorem closure {s : Set X} (hs : IsNowhereDense s) : IsNowhereDense (closure s) := by
  rwa [IsNowhereDense, closure_closure]

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