transfiniteCompositions — Mathlib

English

A specific bound on bottom maps under transfinite composition map.

Русский

Граница на отображения нуля под отображением композиции трансфинитной формы.

LaTeX

$$$\\forall j, b: ⊥ \\to j, W (hf.F.map b)$$$

Lean4

/-- The class of transfinite compositions (for arbitrary well-ordered types `J : Type w`)
of a class of morphisms `W`. -/
@[pp_with_univ]
def transfiniteCompositions : MorphismProperty C :=
  ⨆ (J : Type w) (_ : LinearOrder J) (_ : SuccOrder J) (_ : OrderBot J) (_ : WellFoundedLT J),
    W.transfiniteCompositionsOfShape J

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