English
The complement of a singleton is dense in X if and only if the singleton is not open.
Русский
Дополнение множества, состоящего из одного элемента, плотное в X тогда и только тогда, когда множество {x} не открыто.
LaTeX
$$$Dense({x}^{c}) \iff \neg IsOpen(\{x\})$$$
Lean4
/-- Complement to a singleton is dense if and only if the singleton is not an open set. -/
theorem dense_compl_singleton_iff_not_open : Dense ({ x }ᶜ : Set X) ↔ ¬IsOpen ({ x } : Set X) :=
by
constructor
· intro hd ho
exact (hd.inter_open_nonempty _ ho (singleton_nonempty _)).ne_empty (inter_compl_self _)
· refine fun ho => dense_iff_inter_open.2 fun U hU hne => inter_compl_nonempty_iff.2 fun hUx => ?_
obtain rfl : U = { x } := eq_singleton_iff_nonempty_unique_mem.2 ⟨hne, hUx⟩
exact ho hU
