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.

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) :

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) :

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) :

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) :

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) :

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