ofComposableArrows — Mathlib

English

If f is a transfinite composition of shape J and J′ is order-isomorphic to J, then there exists a transfinite composition of shape J′ for f.

Русский

Если f — трансфинитная композиция формы J, и J′ изоморфно J как упорядочение, то существует трансфинитная композиция формы J′ для f.

LaTeX

$$$\exists \text{OrderIso}(J',J) \Rightarrow \text{TransfiniteCompositionOfShape}(J', f)$$$

Lean4

/-- If `G : ComposableArrows C n`, then `G.hom : G.left ⟶ G.right` is a
transfinite composition of shape `Fin (n + 1)`. -/
@[simps]
def ofComposableArrows {n : ℕ} (G : ComposableArrows C n) : TransfiniteCompositionOfShape (Fin (n + 1)) G.hom
    where
  F := G
  isoBot := Iso.refl _
  incl := _
  isColimit := colimitOfDiagramTerminal (Fin.isTerminalLast n) G
  fac := Category.id_comp _

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