instWeakEquivalenceITrivialCofibrationsFibrations

Mathlib.AlgebraicTopology.ModelCategory.Instances

URI: https://scilib.ai/kg/mathlib#HomotopicalAlgebra.instWeakEquivalenceITrivialCofibrationsFibrations

English

If MapFactorizationData is given from trivialCofibrations to fibrations, then h.i is a WeakEquivalence.

Русский

Если MapFactorizationData задано через тривиальные кофибрации к фибрациям, то h.i является слабой эквивалентностью.

LaTeX

$$$\mathrm{WeakEquivalence}(h.i)$$$

Lean4

instance : WeakEquivalence h.i := by simpa only [weakEquivalence_iff] using h.hi.2

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

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

Разделы

Аффилиация

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