Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-05 12:20 7df0e350

View on Github →

chore(topology): sanity_check pass (#1510)

chore(topology): sanity_check pass
fix(topology/uniform_space/separation): fix build
fix(topology/metric_space): some more namespace fixes

Estimated changes

Modified src/topology/algebra/open_subgroup.lean

modified theorem open_subgroup.is_closed

modified theorem open_subgroup.is_open_of_nonempty_open_subset

modified theorem open_subgroup.is_open_of_open_subgroup

Modified src/topology/algebra/uniform_ring.lean

Modified src/topology/constructions.lean

modified theorem is_open_prod_iff'

Modified src/topology/metric_space/gromov_hausdorff.lean

Modified src/topology/metric_space/isometry.lean

deleted def Kuratowski_embedding.Kuratowski_embedding

deleted theorem Kuratowski_embedding.Kuratowski_embedding_isometry

deleted def Kuratowski_embedding.nonempty_compacts.Kuratowski_embedding

deleted def Kuratowski_embedding.ℓ_infty_ℝ

added def Kuratowski_embedding

added def nonempty_compacts.Kuratowski_embedding

added def ℓ_infty_ℝ

Modified src/topology/stone_cech.lean

Modified src/topology/uniform_space/separation.lean