Theorems · Theorem · category theory

UniformSpaceCat.extensionHom_val

∀ {X : UniformSpaceCat} {Y : CpltSepUniformSpace}
  (f : X ⟶ (CategoryTheory.forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y)
  (x : (UniformSpaceCat.completionFunctor.obj X).α),
  (CategoryTheory.ConcreteCategory.hom (UniformSpaceCat.extensionHom f)) x =
    UniformSpace.Completion.extension (⇑(CategoryTheory.ConcreteCategory.hom f)) x

Defined in

Mathlib.Topology.Category.UniformSpace

Cited by

0 results in Mathlib

Foundations

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