English
A retract of a transfinite composition built from pushouts and coproducts inherits bounds from rl p and ll p, i.e., retracts ≤ W.rlp.llp.
Русский
Обратное отображение трансфинитной композиции, построенной из pushouts и coproducts, наследует границы от rl p и ll p: retracts ≤ W.rlp.llp.
LaTeX
$$$$ \text{retracts}(\text{transfiniteCompositionsPushoutsCoproducts}) \le W.rlp.llp $$$$
Lean4
theorem retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp :
(transfiniteCompositions.{w} (coproducts.{w} W).pushouts).retracts ≤ W.rlp.llp :=
by
rw [le_llp_iff_le_rlp, rlp_retracts, ← le_llp_iff_le_rlp]
apply transfiniteCompositions_pushouts_coproducts_le_llp_rlp
