English
Equality of function-like coercions between morphisms in TopCat and continuous maps coincides.
Русский
Эквивалентность двух определений приведения функций между морфизмами в TopCat и непрерывными отображениями совпадает.
LaTeX
$$$\\text{coe\_of\_of} : \\text{coercions} = \\text{rfl}$$$
Lean4
/-- Replace a function coercion for a morphism `TopCat.of X ⟶ TopCat.of Y` with the definitionally
equal function coercion for a continuous map `C(X, Y)`.
-/
@[simp]
theorem coe_of_of {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {x} :
@DFunLike.coe (TopCat.of X ⟶ TopCat.of Y) ((CategoryTheory.forget TopCat).obj (TopCat.of X))
(fun _ ↦ (CategoryTheory.forget TopCat).obj (TopCat.of Y)) HasForget.instFunLike (ofHom f) x =
@DFunLike.coe C(X, Y) X (fun _ ↦ Y) _ f x :=
rfl
