equivIsoColimit_symm_apply — Mathlib

English

If i is an isomorphism between cocones r and t, then the symmetric equivalence applied to P is equal to P.ofIsoColimit i.symm.

Русский

Если i — изоморфизм коконов r и t, то симметричная эквиваленция применяется к P так же как P.ofIsoColimit i.symm.

LaTeX

$$$ (equivIsoColimit i).symm\, P = P.ofIsoColimit i.symm $$$

Lean4

@[simp]
theorem equivIsoColimit_symm_apply {r t : Cocone F} (i : r ≅ t) (P : IsColimit t) :
    (equivIsoColimit i).symm P = P.ofIsoColimit i.symm :=
  rfl

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