# 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`

.

A complete nontrivially normed field has cardinality at least continuum.

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

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`

.

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

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

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

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