extension_comp_coe — Mathlib

English

The extension from a completion to a uniform space composes with another map to yield the same result as the extension of the composite morphism.

Русский

Расширение композиции с дополнением совпадает с расширением композиции соответствующих отображений.

LaTeX

$$$\mathrm{extensionHom}(\mathrm{completionHom}(X) \circ f)=f$$$

Lean4

@[simp]
theorem extension_comp_coe {X : UniformSpaceCat} {Y : CpltSepUniformSpace}
    (f : toUniformSpace (CpltSepUniformSpace.of (Completion X)) ⟶ toUniformSpace Y) :
    extensionHom (completionHom X ≫ f) = f := by
  ext x
  exact congr_fun (Completion.extension_comp_coe f.hom.property) x

Похожие утверждения