of_pushout_inl_of_codescendsAlong

English

In a pushout square Z → X, Z → Y with pushout X ⊔_Z Y, if Q f holds for the left leg f: Z → X and P holds for the left leg inl: X → pushout, then P also holds for the right leg g: Z → Y. More formally, from Q f and P (pushout.inl f g) we obtain P g.

Русский

В квадрате пушаута Z → X, Z → Y с пушаутом X ⊔_Z Y: если свойство Q выполняется для левого ребра f: Z → X и свойство P выполняется для левого ребра inl: X → пушаут, то свойство P выполняется и для правого ребра g: Z → Y.

LaTeX

$$[P.CodescendsAlong Q] [HasPushout f g] (hf : Q f) (hinl : P (pushout.inl f g)) : P g$$

Lean4

theorem of_pushout_inl_of_codescendsAlong [P.CodescendsAlong Q] [HasPushout f g] (hf : Q f)
    (hinl : P (pushout.inl f g)) : P g :=
  of_isPushout_of_codescendsAlong (.of_hasPushout f g) hf hinl

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