diff_finite — Mathlib

English

Removing a finite set from a dense set preserves density in spaces without isolated points, under mild hypotheses.

Русский

Удаление конечного множества из плотного множества сохраняет плотность при условии отсутствия изолированных точек.

LaTeX

$$$\text{Dense}(s) \Rightarrow \text{Dense}(s \setminus t)$ for finite t.$$

Lean4

/-- Removing a finite set from a dense set in a space without isolated points, one still
obtains a dense set. -/
theorem diff_finite [T1Space X] [∀ x : X, NeBot (𝓝[≠] x)] {s : Set X} (hs : Dense s) {t : Set X} (ht : t.Finite) :
    Dense (s \ t) := by
  convert hs.diff_finset ht.toFinset
  exact (Finite.coe_toFinset _).symm

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