transfiniteCompositions_le — Mathlib

English

If W is stable under transfinite composition, then transfiniteCompositions ≤ W.

Русский

Если W стабильно по трансфинитной композиции, тогда transfiniteCompositions ≤ W.

LaTeX

$$$[IsStableUnderTransfiniteComposition] => transfiniteCompositions(W) \\le W$$$

Lean4

theorem transfiniteCompositions_le [IsStableUnderTransfiniteComposition.{w} W] : transfiniteCompositions.{w} W ≤ W :=
  by
  intro _ _ f hf
  rw [transfiniteCompositions_iff] at hf
  obtain ⟨J, _, _, _, _, hf⟩ := hf
  exact W.transfiniteCompositionsOfShape_le J _ hf

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