English
In a nontrivial topological vector space over a complete nontrivially normed field, any countable set has a dense complement.
Русский
В непустом топологическом векторном пространстве над полем с полным нормированием любая счётная подмножество имеет плотный допольнитель.
LaTeX
$$$s.Countable \\Rightarrow Dense(s^c)$.$$
Lean4
/-- In a nontrivial topological vector space over a complete nontrivially normed field, any
countable set has dense complement. -/
theorem dense_compl {E : Type u} (𝕜 : Type*) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [Module 𝕜 E]
[Nontrivial E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {s : Set E} (hs : s.Countable) :
Dense sᶜ := by
rw [← interior_eq_empty_iff_dense_compl]
by_contra H
apply lt_irrefl (ℵ₀ : Cardinal.{u})
calc
(ℵ₀ : Cardinal.{u}) < 𝔠 := aleph0_lt_continuum
_ ≤ #(interior s) := (continuum_le_cardinal_of_isOpen 𝕜 isOpen_interior (notMem_singleton_empty.1 H))
_ ≤ #s := (mk_le_mk_of_subset interior_subset)
_ ≤ ℵ₀ := le_aleph0 hs
