Commit 2024-09-20 03:09 94db6790

View on Github →

feat(Topology/UniformSpace): Subtype.isComplete_iff (#16730) In the style of Subtype.isCompact_iff

Estimated changes

Modified Mathlib/Topology/UniformSpace/UniformEmbedding.lean

added theorem Subtype.isComplete_iff

added theorem UniformEmbedding.isComplete_iff

added theorem UniformInducing.isComplete_iff