universally_isStableUnderBaseChange

English

If P is stable under base change, then the universally extended P is stable under base change.

Русский

Если P устойчиво к изменению основания, то универсально расширенное P устойчиво к базовым изменениям.

LaTeX

$$$P^{\mathrm{universally}}.IsStableUnderBaseChange$$$

Lean4

instance universally_isStableUnderBaseChange (P : MorphismProperty C) : P.universally.IsStableUnderBaseChange where
  of_isPullback H h₁ _ _ _ _ _ H' := h₁ _ _ _ (H'.paste_vert H.flip)

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