Commit 2024-09-29 14:59 54358ec9
View on Github →feat(UniformEmbedding): add UniformInducing.completeSpace_congr (#17238)
This is a version of _root_.completeSpace_congr
that applies to uniform inducing quotient maps.
Also add ULift.completeSpace_iff and UniformInducing.completeSpace.
I'm going to use these lemmas to generalize some CompleteSpace instances,
see #17244.