hom_ofHom — Mathlib

English

The morphism obtained from a continuous map via ofHom has its hom component equal to that map.

Русский

Морфизм, полученный из непрерывного отображения через ofHom, имеет компоненту hom равной самому отображению.

LaTeX

$$$\\mathrm{TopCat}.Hom(\\mathrm{ofHom}(f)) = f$$$

Lean4

@[simp]
theorem hom_ofHom {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : (ofHom f).hom = f :=
  rfl

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