IsStableUnderInfiniteComposition — Mathlib

English

Equivalence between transfinite compositions defined via W and via the shape J.

Русский

Эквивалентность трансфинитных композиций, определяемых через W и через форму J.

LaTeX

$$$transfiniteCompositions.{w} W f \\equiv W.transfiniteCompositionsOfShape J f$$$

Lean4

/-- A class of morphisms `W : MorphismProperty C` is stable under infinite composition
if for any functor `F : ℕ ⥤ C` such that `F.obj n ⟶ F.obj (n + 1)` is in `W` for any `n : ℕ`,
the map `F.obj 0 ⟶ c.pt` is in `W` for any colimit cocone `c : Cocone F`. -/
abbrev IsStableUnderInfiniteComposition : Prop :=
  W.IsStableUnderTransfiniteCompositionOfShape ℕ

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