transfiniteCompositions_le_llp_rlp

English

The family of transfinite compositions indexed by W is bounded above by the left lifting property against rl p; i.e., transfiniteCompositions.{w} W ≤ W.rlp.llp.

Русский

Семейство трансфинитных композиции, индексированное W, ограничено слева свойством подъема против rl p; то есть transfiniteCompositions.{w} W ≤ W.rlp.llp.

LaTeX

$$$$ \text{transfiniteCompositions}^{w} W \le W.rlp.llp $$$$

Lean4

theorem transfiniteCompositions_le_llp_rlp : transfiniteCompositions.{w} W ≤ W.rlp.llp :=
  by
  intro _ _ f hf
  rw [transfiniteCompositions_iff] at hf
  obtain ⟨_, _, _, _, _, hf⟩ := hf
  exact W.transfiniteCompositionsOfShape_le_llp_rlp _ _ hf

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