# Documentation

Mathlib.Topology.Algebra.Module.Cardinality

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

theorem continuum_le_cardinal_of_module (𝕜 : Type u) (E : Type v) [] [] [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] [] [] {s : Set E} (hs : s nhds 0) :

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] [] [] [] {s : Set E} {x : E} (hs : s nhds x) :

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] [] [] [] {s : Set E} (hs : ) (h'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) [] [] [Module 𝕜 E] [] [] [] [] {s : Set E} (hs : ) (h'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) [] [] [Module 𝕜 E] [] [] [] [] {s : Set E} (hs : ) :

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