Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-26 12:20 11114823

View on Github →

feat(topology/bases): separable subsets of topological spaces (#12936)

Estimated changes

Modified src/topology/bases.lean

added theorem set.countable.is_separable

added theorem set.finite.is_separable

added theorem topological_space.is_separable.closure

added theorem topological_space.is_separable.image

added theorem topological_space.is_separable.mono

added theorem topological_space.is_separable.union

added def topological_space.is_separable

added theorem topological_space.is_separable_Union

added theorem topological_space.is_separable_of_separable_space

added theorem topological_space.is_separable_of_separable_space_subtype

added theorem topological_space.is_separable_univ_iff

added theorem topological_space.separable_space_of_dense_range

Modified src/topology/constructions.lean

added theorem embedding.cod_restrict

added theorem inducing.cod_restrict

Modified src/topology/metric_space/basic.lean

added theorem continuous_on.is_separable_image

added theorem is_compact.is_separable

added theorem metric.dense_iff

added theorem metric.dense_range_iff

modified theorem metric.mem_closure_iff

modified theorem metric.mem_closure_range_iff

modified theorem metric.mem_closure_range_iff_nat

modified theorem metric.mem_of_closed'

added theorem topological_space.is_separable.separable_space