instIsVeryGoodSymmOfRespectsIsoFibrations

Mathlib.AlgebraicTopology.ModelCategory.PathObject

URI: https://scilib.ai/kg/mathlib#HomotopicalAlgebra.PathObject.instIsVeryGoodSymmOfRespectsIsoFibrations

English

If the fibrations respect isomorphisms, then P.symm is VeryGood.

Русский

Если фибрации сохраняют изоморфрам, то P.symm — VeryGood.

LaTeX

$$P.symm.IsVeryGood$$

Lean4

instance [(fibrations C).RespectsIso] [HasBinaryProducts C] [P.IsVeryGood] : P.symm.IsVeryGood where
  cofibration_ι := by dsimp; infer_instance

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

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

Разделы

Аффилиация

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