mem_weakEquivalences

Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations

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

English

If f is a WeakEquivalence, then WeakEquivalences C f.

Русский

Если f — слабое эквалентное отображение, то f принадлежит классу слабых эквалентностей.

LaTeX

$$$WeakEquivalence f \Rightarrow\ weakEquivalences\ C\ f$$$

Lean4

theorem mem_weakEquivalences [WeakEquivalence f] : weakEquivalences C f :=
  WeakEquivalence.mem

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

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

Разделы

Аффилиация

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