English
If s is dense and t is a finite set, then s \ t is dense (in a T1 space with a suitable nonempty punctured neighborhood condition).
Русский
Если s плотное и t конечное множество, то s \ t также плотное (при условии существования непустого дырчатого окрестности).
LaTeX
$$$\text{Dense}(s) \Rightarrow \text{Dense}(s \setminus t)$ for finite t (with hypotheses on nhds within x).$$
Lean4
/-- Removing a finset from a dense set in a space without isolated points, one still
obtains a dense set. -/
theorem diff_finset [T1Space X] [∀ x : X, NeBot (𝓝[≠] x)] {s : Set X} (hs : Dense s) (t : Finset X) : Dense (s \ t) :=
by
classical
induction t using Finset.induction_on with
| empty => simpa using hs
| insert _ _ _ ih =>
rw [Finset.coe_insert, ← union_singleton, ← diff_diff]
exact ih.diff_singleton _
