trivialFibrations_llp — Mathlib

English

Cofibrations are exactly the morphisms that have the left lifting property with respect to all trivial fibrations.

Русский

Кофибрации равны по сути по левому пропускному свойству (левому заполнению) относительно всех тривиальных фибраций.

LaTeX

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

Lean4

theorem trivialFibrations_llp : (trivialFibrations C).llp = cofibrations C :=
  llp_eq_of_wfs _ _

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