homOfCone_coneOfHom — Mathlib

English

For any f: Y → X, homOfCone h (coneOfHom h f) = f, i.e., the cone construction reverses the hom-construction.

Русский

Для любого f: Y → X, homOfCone h (coneOfHom h f) = f, то есть конусная конструкция обратна конструированию морфизма.

LaTeX

$$$ homOfCone h (coneOfHom h f) = f $$$

Lean4

@[simp]
theorem homOfCone_coneOfHom {Y : C} (f : Y ⟶ X) : homOfCone h (coneOfHom h f) = f := by simp [coneOfHom, homOfCone]

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