Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-16 22:44 7dae87fe

View on Github →

feat(topology/metric_space/basic): ext lemmas for metric spaces (#12070) Also add a few results in metric_space.basic:

A decreasing intersection of closed sets with diameter tending to 0 is nonempty in a complete space
new constructions of metric spaces by pulling back structures (and adjusting definitional equalities)
fixing metric_space empty and metric_space punit to make sure the uniform structure is definitionally the right one.

Estimated changes

Modified src/order/filter/basic.lean

added theorem filter.eq_top_of_ne_bot

Modified src/topology/metric_space/basic.lean

added theorem cauchy_seq_of_le_tendsto_0'

added theorem dense.exists_dist_lt

added theorem dense_range.exists_dist_lt

added def embedding.comap_metric_space

added theorem is_complete.nonempty_Inter_of_nonempty_bInter

added theorem metric.nonempty_Inter_of_nonempty_bInter

added theorem metric_space.ext

added def metric_space.replace_topology

added theorem metric_space.replace_topology_eq

added theorem metric_space.replace_uniformity_eq

added theorem pseudo_metric_space.ext

added theorem pseudo_metric_space.replace_uniformity_eq

modified def uniform_embedding.comap_metric_space

Modified src/topology/uniform_space/basic.lean