universally_eq

Mathlib.CategoryTheory.MorphismProperty.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.IsStableUnderBaseChange.universally_eq

English

If P is stable under base change, then P.universally = P.

Русский

Если P устойчиво к изменению основания, то P.universally = P.

LaTeX

$$$P^{\mathrm{universally}} = P$$$

Lean4

theorem universally_eq {P : MorphismProperty C} [hP : P.IsStableUnderBaseChange] : P.universally = P :=
  universally_eq_iff.mpr hP

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru