instWeakEquivalencePTrivialCofibrationsFibrations

Mathlib.AlgebraicTopology.ModelCategory.BrownLemma

URI: https://scilib.ai/kg/mathlib#HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalencePTrivialCofibrationsFibrations

English

For a FibrantBrownFactorization f, if f is a WeakEquivalence then h.p is a WeakEquivalence.

Русский

Для FibrantBrownFactorization f, если f — слабое эквалентное отображение, то h.p — слабое эквалентное отображение.

LaTeX

$$$[\WeakEquivalence f] \Rightarrow \WeakEquivalence h.p$$$

Lean4

instance [WeakEquivalence f] : WeakEquivalence h.p :=
  weakEquivalence_of_precomp_of_fac h.fac

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

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

Разделы

Аффилиация

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