dense_iff_closure_eq — Mathlib

English

A subset s of a topological space X is dense if and only if its closure is the whole space: Dense(s) ↔ closure(s) = univ.

Русский

Подмножество s пространства X плотно тогда и только тогда, когда его замыкание совпадает с всем пространством: Dense(s) ↔ closure(s) = univ.

LaTeX

$$$\\\\overline{s} = \\\\operatorname{univ} \\\\iff \\\\text{Dense}(s)$$$

Lean4

theorem dense_iff_closure_eq : Dense s ↔ closure s = univ :=
  eq_univ_iff_forall.symm

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