cofibrations_rlp — Mathlib

English

Cofibrations have the right lifting property with respect to trivial fibrations; equivalently, (cofibrations(C)).rlp = trivialFibrations(C).

Русский

Кофибрации обладают правым свойством заполнения по отношению к тривиальным фибрациям; эквивалентно (cofibrations(C)).rlp = trivialFibrations(C).

LaTeX

$$$ (\\mathrm{cofibrations}(C)).\\mathrm{RLP} = \\mathrm{trivialFibrations}(C). $$$

Lean4

theorem cofibrations_rlp : (cofibrations C).rlp = trivialFibrations C :=
  rlp_eq_of_wfs _ _

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