trivialCofibrations_rlp — Mathlib

English

The class of trivial cofibrations is stable under cobase change in the presence of a weak factorization system.

Русский

Класс тривиальных кофибраций устойчив под cobase change при наличии слабой факторизационной системы.

LaTeX

$$$\operatorname{IsStableUnderCobaseChange}\big(\operatorname{trivialCofibrations}C\big)$$$

Lean4

theorem trivialCofibrations_rlp : (trivialCofibrations C).rlp = fibrations C :=
  rlp_eq_of_wfs _ _

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