Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-10 15:18 c8738cb6

View on Github →

feat(topology/uniform_space/cauchy): generalize second_countable_of_separable to uniform spaces (#4530) Also generalize is_countably_generated.has_antimono_basis to is_countably_generated.exists_antimono_subbasis and add a few lemmas about bases of the uniformity filter.

Estimated changes

Modified src/order/filter/at_top_bot.lean

Modified src/order/filter/bases.lean

added theorem filter.has_basis.property_index

added theorem filter.has_basis.set_index_mem

added theorem filter.has_basis.set_index_subset

added theorem filter.is_countably_generated.exists_antimono_basis

deleted theorem filter.is_countably_generated.exists_antimono_seq

added theorem filter.is_countably_generated.exists_antimono_subbasis

deleted theorem filter.is_countably_generated.has_antimono_basis

modified theorem filter.is_countably_generated.inf

modified theorem filter.is_countably_generated.inf_principal

modified theorem filter.is_countably_generated_iff_exists_antimono_basis

Modified src/topology/bases.lean

added theorem topological_space.exists_countable_dense

Modified src/topology/basic.lean

Modified src/topology/metric_space/emetric_space.lean

Modified src/topology/sequences.lean

Modified src/topology/uniform_space/basic.lean

modified theorem nhds_eq_uniformity

added theorem uniform_space.is_open_ball

added theorem uniform_space.mem_ball_self

added theorem uniformity_has_basis_open

added theorem uniformity_has_basis_open_symmetric

Modified src/topology/uniform_space/cauchy.lean

added theorem uniform_space.second_countable_of_separable

Modified src/topology/uniform_space/completion.lean