pushout_inl — Mathlib

English

If P is stable under cobase change, then given f,g with HasPushout, P(f) implies P(pushout.inr f g).

Русский

Если P устойчива к cobase change, то при наличии пуш-аутa, P(f) => P(pushout.inr f g).

LaTeX

$$[IsStableUnderCobaseChange P] → (HasPushout f g) → P f → P (pushout.inr f g)$$

Lean4

theorem pushout_inl [IsStableUnderCobaseChange P] {A B A' : C} (f : A ⟶ A') (g : A ⟶ B) [HasPushout f g] (H : P g) :
    P (pushout.inl f g) :=
  of_isPushout (IsPushout.of_hasPushout f g) H

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