hf — Mathlib · SciLib

English

Equality of f with the IsColimit.map expression for the first costructured arrow.

Русский

Равенство f с выражением IsColimit.map для первого CostructuredArrow.

LaTeX

$$$f = \mathrm{IsColimit.map}(\mathrm{isColimit}_1\,f\,g\,P_1\,P_2)\big(\mathrm{Cocone.mk}\ B (\iota_2\,f\,g\,P_1\,P_2)\big)\;\big(\mathrm{whiskerRight}(\varphi\,f\,g\,P_1\,P_2)\ yoneda\big)$$$

Lean4

theorem hf :
    f = IsColimit.map (isColimit₁ f g P₁ P₂) (Cocone.mk B (ι₂ f g P₁ P₂)) (whiskerRight (ϕ f g P₁ P₂) yoneda) :=
  by
  refine (isColimit₁ f g P₁ P₂).hom_ext (fun i => ?_)
  rw [IsColimit.ι_map]
  simpa using i.hom.1.w.symm

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