isStableUnderBaseChange_iff_pullbacks_le

English

IsStableUnderBaseChange is equivalent to P.pullbacks ≤ P.

Русский

Устойчивость к базовому изменению эквивалентна неравенству P.pullbacks ≤ P.

LaTeX

$$P.IsStableUnderBaseChange \iff P.pullbacks ≤ P$$

Lean4

theorem isStableUnderBaseChange_iff_pullbacks_le : P.IsStableUnderBaseChange ↔ P.pullbacks ≤ P :=
  by
  constructor
  · intro h _ _ _ ⟨_, _, _, _, _, h₁, h₂⟩
    exact of_isPullback h₂ h₁
  · intro h
    constructor
    intro _ _ _ _ _ _ _ _ h₁ h₂
    exact h _ ⟨_, _, _, _, _, h₂, h₁⟩

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