pushouts_mk — Mathlib

English

If a square is a pushout and q has property P, then the pushout morphism p has the corresponding pushouts property P.pushouts.

Русский

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

LaTeX

$$IsPushout(f,q,p,g) \land P(q) \Rightarrow P.pushouts(p)$$

Lean4

theorem pushouts_mk {A B X Y : C} {f : A ⟶ X} {q : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} (sq : IsPushout f q p g) (hq : P q) :
    P.pushouts p :=
  ⟨_, _, _, _, _, hq, sq⟩

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