Theorems · Theorem · category theory

UniformSpaceCat.extension_comp_hom

∀ {X : UniformSpaceCat} {Y : CpltSepUniformSpace}
  (f : (CpltSepUniformSpace.of (UniformSpace.Completion X.carrier)).toUniformSpace ⟶ Y.toUniformSpace),
  (UniformSpaceCat.extensionHom (CategoryTheory.CategoryStruct.comp X.completionHom f)).hom = f

Defined in

Mathlib.Topology.Category.UniformSpace

Cited by

0 results in Mathlib

Foundations

Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound