instFibrationP₀

Mathlib.AlgebraicTopology.ModelCategory.PathObject

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

English

If f0 ~ f1 and f1 ~ f2, then f0 ~ f2 (same transitivity under hypotheses).

Русский

Если f0 ~ f1 и f1 ~ f2, то f0 ~ f2 (при соответствующих допущениях).

LaTeX

$$$ f_0 \sim_L f_1 \land f_1 \sim_L f_2 \Rightarrow f_0 \sim_L f_2$$$

Lean4

instance : Fibration P.p₀ := by
  rw [← P.p_fst]
  infer_instance

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

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

Разделы

Аффилиация

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