English
Let P.IsStableUnderCobaseChange and P.CodescendsAlong Q hold, with HasPushout f g. If Q f holds, then P for the left leg of the pushout is equivalent to P for the right leg g; i.e., P(pushout.inl f g) ⇔ P(g).
Русский
Пусть P.IsStableUnderCobaseChange и P.CodescendsAlong Q выполняются, и существует пуш-аут f g. Если Q f, тогда P(левый отрезок пушаута) эквивалентно P(правому отрезку g).
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], (hf : Q f) \Rightarrow (P(\mathrm{pushout.inl} f g) \iff P(g)).$$$
Lean4
theorem pushout_inl_iff [P.IsStableUnderCobaseChange] [P.CodescendsAlong Q] [HasPushout f g] (hf : Q f) :
P (pushout.inl f g) ↔ P g :=
iff_of_isPushout (.of_hasPushout f g) hf
