Commit 2025-10-28 21:01 e43769cf

View on Github →

feat(UniformSpace/Completion): add UniformSpace.Completion.mapEquiv (#30574) If α ≃ᵤ β then Completion α ≃ᵤ Completion β.

Estimated changes

Modified Mathlib/Topology/UniformSpace/AbstractCompletion.lean

added def AbstractCompletion.mapEquiv

added theorem AbstractCompletion.mapEquiv_coe

added theorem AbstractCompletion.mapEquiv_symm

Modified Mathlib/Topology/UniformSpace/Completion.lean

added def UniformSpace.Completion.mapEquiv

added theorem UniformSpace.Completion.mapEquiv_coe

added theorem UniformSpace.Completion.mapEquiv_symm