of_isPushout_of_codescendsAlong — Mathlib

English

If P is stable under cobase change and CodescendsAlong Q, then IsPushout f g inl inr implies Q f and P inl implies P g, and vice versa.

Русский

Если P устойчива к основанию-копированию и CodescendsAlong Q, то IsPushout влечёт Q f и P inl → P g, и обратно.

LaTeX

$$$ [P.IsStableUnderCobaseChange] [P.CodescendsAlong Q] (h : IsPushout f g inl inr) (hg : Q f) : (P inl \\rightarrow P g) \\wedge (P g \\rightarrow P inl)$$$

Lean4

theorem of_isPushout_of_codescendsAlong [P.CodescendsAlong Q] (h : IsPushout f g inl inr) (hf : Q f) (hinl : P inl) :
    P g :=
  CodescendsAlong.of_isPushout h hf hinl

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