instIsFibrantIOfIsVeryGood

Mathlib.AlgebraicTopology.ModelCategory.Cylinder

URI: https://scilib.ai/kg/mathlib#HomotopicalAlgebra.Cylinder.instIsFibrantIOfIsVeryGood

English

If A is fibrant and P is VeryGood, then P.I is fibrant.

Русский

Если A фибрaнтен, а P очень хорош, то P.I фибрантен.

LaTeX

$$$\text{IsFibrant}(P.I)$$$

Lean4

instance [HasBinaryCoproduct A A] [HasTerminal C] [IsFibrant A] [P.IsVeryGood] : IsFibrant P.I :=
  isFibrant_of_fibration P.π

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

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

Разделы

Аффилиация

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