instRespectsIsoPullbacks — Mathlib

English

Pullbacks preserve isomorphisms: the property P on pullbacks is stable under isomorphisms of the pullback square.

Русский

Пуллбэки сохраняют изоморфизмы: свойство P на пуллбэках устойчиво под изоморфизмами квадрата пуллбэков.

LaTeX

$$P.pullbacks.RespectsIso$$

Lean4

instance : P.pullbacks.RespectsIso :=
  RespectsIso.of_respects_arrow_iso _
    (by
      rintro q q' e ⟨X, Y, p, f, g, hp, h⟩
      exact
        ⟨X, Y, p, e.inv.left ≫ f, e.inv.right ≫ g, hp, IsPullback.paste_horiz (IsPullback.of_horiz_isIso ⟨e.inv.w⟩) h⟩)

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