of_pushout_inr_of_descendsAlong — Mathlib

English

Under [P.CodescendsAlong Q] and HasPushout f g, if Q g holds and P holds for the right leg pushout.inr f g, then P holds for f.

Русский

При условии, что P(descends along Q) и существуют пуш-ауты f g, если Q g справедливо и P(правый отрезок pushout.inr f g) выполняется, то P выполняется для f.

LaTeX

$$$\forall {C} [\mathsf{Category} C] {P Q : \mathsf{MorphismProperty} C} {Z X Y : C} {f : Z \rightarrow X} {g : Z \rightarrow Y} [P.CodescendsAlong Q] [\mathsf{Limits.HasPushout} f g], (hg : Q g) (hinr : P(\mathrm{pushout.inr} f g)) \Rightarrow P f.$$$

Lean4

theorem of_pushout_inr_of_descendsAlong [P.CodescendsAlong Q] [HasPushout f g] (hg : Q g) (hinr : P (pushout.inr f g)) :
    P f :=
  of_isPushout_of_codescendsAlong (IsPushout.of_hasPushout f g).flip hg hinr

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