iff_of_isPushout — Mathlib

English

If P is stable under cobase change and CodescendsAlong Q, then P on inl is equivalent to P on g for pushout f,g with inl and inr.

Русский

Если P устойчива к базовым изменениям и CodescendsAlong Q, то P на inl эквивалентно P на g для пушаута f,g с inl и inr.

LaTeX

$$[P.IsStableUnderCobaseChange] [P.CodescendsAlong Q] (IsPushout f g inl inr) (hg : Q f) : P inl ↔ P g$$

Lean4

theorem iff_of_isPushout [P.IsStableUnderCobaseChange] [P.CodescendsAlong Q] (h : IsPushout f g inl inr) (hg : Q f) :
    P inl ↔ P g :=
  ⟨fun hinl ↦ of_isPushout_of_codescendsAlong h hg hinl, fun hf ↦ P.of_isPushout h hf⟩

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