pushout_inr — Mathlib

English

If P is stable under cobase change, then P(g) implies P(pushout.inl f g) in HasPushout f g.

Русский

Если P устойчива к cobase change, то P(g) → P(pushout.inl f g) при HasPushout f g.

LaTeX

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

Lean4

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

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