English
The transfinite compositions of shape pushouts and coproducts preserve the left lifting property against a fixed right lifting property, i.e., W.transfiniteCompositionsOfShape J ≤ W.rlp.llp.
Русский
Трансфинитные композиции формы pushouts и coproducts сохраняют свойство подъёма слева по отношению к фиксированному правому свойству подъёма: W.transfiniteCompositionsOfShape J ≤ W.rlp.llp.
LaTeX
$$$$ W.transfiniteCompositionsOfShape J \le W.rlp.llp $$$$
Lean4
theorem transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp :
(coproducts.{w} W).pushouts.transfiniteCompositionsOfShape J ≤ W.rlp.llp := by
simpa using transfiniteCompositionsOfShape_le_llp_rlp (coproducts.{w} W).pushouts J
