equivIsoLimit — Mathlib

English

Given two cones r and t over F and an isomorphism i: r ≅ t, there is an equivalence of the type IsLimit r ≃ IsLimit t. This expresses that being a limit cone is preserved by isomorphisms of cones.

Русский

Пусть r и t — конусы над F и дано изоморфизм i: r ≅ t. Тогда существует эквивариантность IsLimit r ≃ IsLimit t, т. е. свойство предела сохраняется под изоморфизм конусов.

LaTeX

$$$\\text{equivIsoLimit }i:\\ IsLimit(r) \\simeq IsLimit(t)$$$

Lean4

/-- Isomorphism of cones preserves whether or not they are limiting cones. -/
def equivIsoLimit {r t : Cone F} (i : r ≅ t) : IsLimit r ≃ IsLimit t
    where
  toFun h := h.ofIsoLimit i
  invFun h := h.ofIsoLimit i.symm
  left_inv := by cat_disch
  right_inv := by cat_disch

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