of_isPullback — Mathlib

English

If there exists an IsPullback h: fst snd f, and P f, then P snd.

Русский

Если существует IsPullback h: fst snd f, и P f, тогда P snd.

LaTeX

$$∀{f}, IsPullback fst snd f (𝒰.f i) → P f → P snd$$

Lean4

theorem of_isPullback {X' : C} (i : 𝒰.I₀) {fst : X' ⟶ X} {snd : X' ⟶ 𝒰.X i} (h : IsPullback fst snd f (𝒰.f i))
    (hf : P f) : P snd :=
  by
  rw [← P.cancel_left_of_respectsIso h.isoPullback.inv, h.isoPullback_inv_snd]
  exact pullbackSnd _ _ hf

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