equivIsoColimit_apply — Mathlib

English

The equivalence equivIsoColimit applied to an IsColimit structure P on r gives P.ofIsoColimit i when i is the isomorphism between cocones.

Русский

Применение эквивалентности equivIsoColimit к структуре IsColimit P над коконом r дает P.ofIsoColimit i, когда i — изоморфизм коконов.

LaTeX

$$$ equivIsoColimit i\, P = P.ofIsoColimit i $$$

Lean4

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

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