English
Let P be a property of morphisms in a category C which is stable under cobase change. In a pushout square with arrows g, f, f', g', if the left edge f has property P, then the right edge f' also has property P.
Русский
Пусть P — свойство морфизмов в категории C, устойчивое при базовом изменении (по пуш-ауту). В квадрате пуш-аут с стрелками g, f, f', g', если левый ребро f удовлетворяет свойству P, то и правый ребро f' удовлетворяет свойству P.
LaTeX
$$$\forall \{A,A',B,B'\} \; {f:\,A\to A'},\; {g:\,A\to B},\; {f':B\to B'},\; {g':A'\to B'},\; (\text{IsPushout } g\ f\ f'\ g')\; \rightarrow\; P(f) \rightarrow P(f').$$$
Lean4
theorem of_isPushout [P.IsStableUnderCobaseChange] {A A' B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'}
(sq : IsPushout g f f' g') (hf : P f) : P f' :=
IsStableUnderCobaseChange.of_isPushout sq hf
