English
Let s be a subset of a topological space X. Then s is dense in X if and only if every nonempty open set intersects s.
Русский
Пусть s ⊆ X. Тогда s плотно в X тогда и только тогда, когда пересечение s с любым непустым открытым множеством непусто.
LaTeX
$$$\operatorname{Dense}(s) \iff \forall U, \mathrm{IsOpen}(U) \rightarrow U \neq \emptyset \rightarrow (U \cap s) \neq \emptyset$$$
Lean4
/-- A set is dense if and only if it has a nonempty intersection with each nonempty open set. -/
theorem dense_iff_inter_open : Dense s ↔ ∀ U, IsOpen U → U.Nonempty → (U ∩ s).Nonempty :=
by
constructor <;> intro h
· rintro U U_op ⟨x, x_in⟩
exact mem_closure_iff.1 (h _) U U_op x_in
· intro x
rw [mem_closure_iff]
intro U U_op x_in
exact h U U_op ⟨_, x_in⟩
