# 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) [] [CompleteSpace ๐] :

A complete nontrivially normed field has cardinality at least continuum.

theorem continuum_le_cardinal_of_module (๐ : Type u) (E : Type v) [] [CompleteSpace ๐] [] [Module ๐ 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) [] [] [Module ๐ E] [] [ContinuousSMul ๐ E] {s : Set E} (hs : s โ nhds 0) :
Cardinal.mk โs =

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) [] [] [Module ๐ E] [] [] [ContinuousSMul ๐ E] {s : Set E} {x : E} (hs : s โ nhds x) :
Cardinal.mk โs =

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) [] [] [Module ๐ E] [] [] [ContinuousSMul ๐ E] {s : Set E} (hs : ) (h's : s.Nonempty) :
Cardinal.mk โs =

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) [] [CompleteSpace ๐] [] [Module ๐ E] [] [] [] [ContinuousSMul ๐ E] {s : Set E} (hs : ) (h's : s.Nonempty) :

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) [] [CompleteSpace ๐] [] [Module ๐ E] [] [] [] [ContinuousSMul ๐ E] {s : Set E} (hs : s.Countable) :

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