homOfCocone_coconeOfHom — Mathlib

English

If F.cocones is corepresented by X, then homOfCocone h (coconeOfHom h f) = f for any f : X ⟶ Y.

Русский

Если коконы F над X корпредставлены X, то для любого f : X ⟶ Y выполняется homOfCocone h (coconeOfHom h f) = f.

LaTeX

$$$\mathrm{homOfCocone}\ h\; (\mathrm{coconeOfHom}\ h\; f) = f$$$

Lean4

@[simp]
theorem homOfCocone_coconeOfHom {Y : C} (f : X ⟶ Y) : homOfCocone h (coconeOfHom h f) = f := by
  simp [homOfCocone, coconeOfHom]

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