le_transfiniteCompositions — Mathlib

English

The transfinite compositions class is below the original property W in the lattice order.

Русский

Класс трансфинитных композиций лежит ниже исходного свойства W в частично упорядоченной решетке.

LaTeX

$$$transfiniteCompositions(W) \\le W$$$

Lean4

theorem le_transfiniteCompositions : W ≤ transfiniteCompositions.{w} W :=
  le_trans
    (fun _ _ _ hf ↦
      (MorphismProperty.TransfiniteCompositionOfShape.ofOrderIso (.ofMem _ hf) (orderIsoShrink.{w} (Fin 2)).symm).mem)
    (transfiniteCompositionsOfShape_le_transfiniteCompositions _ _)

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