isStableUnderCobaseChange_iff_pushouts_le

English

For a property P, P is stable under cobase change if and only if the pushouts of P are contained in P; i.e., the pushouts operator is ≤ with respect to P.

Русский

Для свойства P верно: P устойчиво к cobase change тогда и только тогда, когда все пуш-ауты, получаемые из P, принадлежат P; то есть операция пуш-аутов меньше или равна P.

LaTeX

$$$P\IsStableUnderCobaseChange \iff\ P.pushouts \le P$.$$

Lean4

theorem isStableUnderCobaseChange_iff_pushouts_le : P.IsStableUnderCobaseChange ↔ P.pushouts ≤ P :=
  by
  constructor
  · intro h _ _ _ ⟨_, _, _, _, _, h₁, h₂⟩
    exact of_isPushout h₂ h₁
  · intro h
    constructor
    intro _ _ _ _ _ _ _ _ h₁ h₂
    exact h _ ⟨_, _, _, _, _, h₂, h₁⟩

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