Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-15 14:39 b0508f3c

View on Github →

feat(topology/uniform/uniform_embedding): a sum of two complete spaces is complete (#11971)

Estimated changes

Modified src/topology/uniform_space/basic.lean

added theorem discrete_topology_of_discrete_uniformity

modified def uniform_space.replace_topology

Modified src/topology/uniform_space/uniform_embedding.lean

added def embedding.comap_uniform_space

added theorem embedding.to_uniform_embedding

added theorem uniform_embedding_inl

added theorem uniform_embedding_inr