instWeakEquivalencePCofibrationsTrivialFibrations

English

If f has a MapFactorizationData (cofibrations) (trivialFibrations) f, then the p-part is a WeakEquivalence.

Русский

Если у отображения f есть MapFactorizationData (кофибрации) (тривиальные фибрации) f, то компонент p является слабой эквивалентностью.

LaTeX

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

Lean4

instance : WeakEquivalence h.p := by simpa only [weakEquivalence_iff] using h.hp.2

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