pushout_inr_iff — Mathlib

English

If P.IsStableUnderCobaseChange and P.CodescendsAlong Q, and HasPushout f g, then P(pushout.inr f g) ↔ P f when Q g holds.

Русский

Если P стабилен по вершине и PDescendsAlong Q, существует пуш-аут f g, и Q g выполняется, то P(правый отрезок) эквивалентно 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.IsStableUnderCobaseChange] [P.CodescendsAlong Q] [\mathsf{Limits.HasPushout} f g], (hg : Q g) \Rightarrow P(\mathrm{pushout.inr} f g) \iff P(f).$$$

Lean4

theorem pushout_inr_iff [P.IsStableUnderCobaseChange] [P.CodescendsAlong Q] [HasPushout f g] (hg : Q g) :
    P (pushout.inr f g) ↔ P f :=
  iff_of_isPushout (IsPushout.of_hasPushout f g).flip hg

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