Commit 2023-02-05 01:25 713bcc99

View on Github →

feat: port Topology.UniformSpace.CompleteSeparated (#2063)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/UniformSpace/CompleteSeparated.lean

added theorem DenseInducing.continuous_extend_of_cauchy

added theorem IsComplete.isClosed