ici — Mathlib

English

For every n, a nonzero index exists in Fin(n+1); thereby a base for the transfinite composition exists.

Русский

Для каждого n существует ненулевой индекс в Fin(n+1); таким образом задаётся базовый индекс трансфинитной композиции.

LaTeX

$$$\mathrm{NeZero}(\mathrm{Fin}(n+1))$$$

Lean4

/-- A transfinite composition of shape `J` induces a transfinite composition
of shape `Set.Ici j` for any `j : J`. -/
@[simps]
noncomputable def ici (j : J) : TransfiniteCompositionOfShape (Set.Ici j) (c.incl.app j)
    where
  F := (Subtype.mono_coe (Set.Ici j)).functor ⋙ c.F
  isWellOrderContinuous := Functor.IsWellOrderContinuous.restriction_setIci _
  isoBot := Iso.refl _
  incl := Functor.whiskerLeft _ c.incl
  isColimit := (Functor.Final.isColimitWhiskerEquiv ((Subtype.mono_coe (Set.Ici j)).functor) _).2 c.isColimit

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