English
There is a natural isomorphism between the completion of a uniform space and the completion of its separation quotient.
Русский
Существует естественное изоморфизм завершения для равномерного пространства и для его отделяющего фактора.
LaTeX
$$$\\mathrm{Completion}(\\mathrm{SeparationQuotient}(\\alpha)) \\cong \\mathrm{Completion}(\\alpha)$$$
Lean4
/-- The isomorphism between the completion of a uniform space and the completion of its separation
quotient. -/
def completionSeparationQuotientEquiv (α : Type u) [UniformSpace α] :
Completion (SeparationQuotient α) ≃ Completion α :=
by
refine
⟨Completion.extension (lift' ((↑) : α → Completion α)), Completion.map SeparationQuotient.mk, fun a ↦ ?_, fun a ↦
?_⟩
· refine induction_on a (isClosed_eq (continuous_map.comp continuous_extension) continuous_id) ?_
refine SeparationQuotient.surjective_mk.forall.2 fun a ↦ ?_
rw [extension_coe (uniformContinuous_lift' _), lift'_mk (uniformContinuous_coe α), map_coe uniformContinuous_mk]
· refine induction_on a (isClosed_eq (continuous_extension.comp continuous_map) continuous_id) fun a ↦ ?_
rw [map_coe uniformContinuous_mk, extension_coe (uniformContinuous_lift' _), lift'_mk (uniformContinuous_coe _)]
