of_iso — Mathlib

English

If sq1 isPullback and e: sq1 ≅ sq2 is an isomorphism, then sq2 isPullback.

Русский

Если sq1 — pullback и есть изоморфизм e: sq1 ≅ sq2, то sq2 — pullback.

LaTeX

$$sq2.IsPullback$$

Lean4

theorem of_iso {sq₁ sq₂ : Square C} (h : sq₁.IsPullback) (e : sq₁ ≅ sq₂) : sq₂.IsPullback :=
  by
  refine
    CategoryTheory.IsPullback.of_iso h (evaluation₁.mapIso e) (evaluation₂.mapIso e) (evaluation₃.mapIso e)
      (evaluation₄.mapIso e) ?_ ?_ ?_ ?_
  all_goals simp

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