Commit 2023-08-19 18:38 c6ffbe85

View on Github →

feat: a countable set has dense complement in a nontrivial vector space over a complete normed field (#6556)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Module/Cardinality.lean

added theorem Set.Countable.dense_compl

added theorem cardinal_eq_of_is_open

added theorem cardinal_eq_of_mem_nhds

added theorem cardinal_eq_of_mem_nhds_zero

added theorem continuum_le_cardinal_of_is_open

added theorem continuum_le_cardinal_of_module

added theorem continuum_le_cardinal_of_nontriviallyNormedField