dense_closure — Mathlib

English

The closure of a set is dense if and only if the set itself is dense: Dense(closure s) ↔ Dense(s).

Русский

Замыкание множества плотно тогда, когда само множество плотно: Dense(closure s) ↔ Dense(s).

LaTeX

$$$\\\\text{Dense}(closure(s)) \\\\iff \\\\text{Dense}(s)$$$

Lean4

/-- The closure of a set `s` is dense if and only if `s` is dense. -/
@[simp]
theorem dense_closure : Dense (closure s) ↔ Dense s := by rw [Dense, Dense, closure_closure]

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