instWeakEquivalenceR

Mathlib.AlgebraicTopology.ModelCategory.BrownLemma

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

English

For a FibrantBrownFactorization f, h is a WeakEquivalence.

Русский

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

LaTeX

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

Lean4

instance : WeakEquivalence h.r :=
  weakEquivalence_of_precomp_of_fac h.i_r

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

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

Разделы

Аффилиация

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