Cardinality of open subsets of vector spaces

Any nonempty open subset of a topological vector space over a nontrivially normed field has the same cardinality as the whole space. This is proved in cardinal_eq_of_isOpen.

We deduce that a countable set in a nontrivial vector space over a complete nontrivially normed field has dense complement, in Set.Countable.dense_compl. This follows from the previous argument and the fact that a complete nontrivially normed field has cardinality at least continuum, proved in continuum_le_cardinal_of_nontriviallyNormedField.

theorem continuum_le_cardinal_of_nontriviallyNormedField (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] : Cardinal.continuum ≤ Cardinal.mk 𝕜

A complete nontrivially normed field has cardinality at least continuum.

theorem continuum_le_cardinal_of_module (𝕜 : Type u) (E : Type v) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nontrivial E] : Cardinal.continuum ≤ Cardinal.mk E

A nontrivial module over a complete nontrivially normed field has cardinality at least continuum.

theorem cardinal_eq_of_mem_nhds_zero {E : Type u_1} (𝕜 : Type u_2) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] {s : Set E} (hs : s ∈ nhds 0) : Cardinal.mk ↑s = Cardinal.mk E

In a topological vector space over a nontrivially normed field, any neighborhood of zero has the same cardinality as the whole space.

See also cardinal_eq_of_mem_nhds.

theorem cardinal_eq_of_mem_nhds {E : Type u_1} (𝕜 : Type u_2) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {s : Set E} {x : E} (hs : s ∈ nhds x) : Cardinal.mk ↑s = Cardinal.mk E

In a topological vector space over a nontrivially normed field, any neighborhood of a point has the same cardinality as the whole space.

theorem cardinal_eq_of_isOpen {E : Type u_1} (𝕜 : Type u_2) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {s : Set E} (hs : IsOpen s) (h's : s.Nonempty) : Cardinal.mk ↑s = Cardinal.mk E

In a topological vector space over a nontrivially normed field, any nonempty open set has the same cardinality as the whole space.

theorem continuum_le_cardinal_of_isOpen {E : Type u_1} (𝕜 : Type u_2) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nontrivial E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {s : Set E} (hs : IsOpen s) (h's : s.Nonempty) : Cardinal.continuum ≤ Cardinal.mk ↑s

In a nontrivial topological vector space over a complete nontrivially normed field, any nonempty open set has cardinality at least continuum.

theorem Set.Countable.dense_compl {E : Type u} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nontrivial E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {s : Set E} (hs : s.Countable) : Dense sᶜ

In a nontrivial topological vector space over a complete nontrivially normed field, any countable set has dense complement.