pullbacks_mk — Mathlib

English

If a square is a pullback and p has property P, then the induced pullback morphism q has the corresponding pullback property P.pullbacks.

Русский

Если диаграмма является пулбэком и p обладает свойством P, то полученная стрелка q обладает свойством P.pullbacks.

LaTeX

$$IsPullback(f,q,p,g) \land P(p) \Rightarrow P.pullbacks(q)$$

Lean4

theorem pullbacks_mk {A B X Y : C} {f : A ⟶ X} {q : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} (sq : IsPullback f q p g)
    (hp : P p) : P.pullbacks q :=
  ⟨_, _, _, _, _, hp, sq⟩

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