equivIsoLimit_symm_apply — Mathlib

English

For an isomorphism i: r ≅ t and a limit cone P on t, the symmetrized equivalence applied to P yields P.ofIsoLimit i.symm.

Русский

Пусть i: r ≅ t и P — предел на t. Применение симметричной эквивалентности к P даёт P.ofIsoLimit i.symm.

LaTeX

$$$ (\\equivIsoLimit i).symm \\;P = P.ofIsoLimit i.symm $$$

Lean4

@[simp]
theorem equivIsoLimit_symm_apply {r t : Cone F} (i : r ≅ t) (P : IsLimit t) :
    (equivIsoLimit i).symm P = P.ofIsoLimit i.symm :=
  rfl

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