transfiniteCompositionsOfShape — Mathlib

English

Given W and a well-ordered type J, the class transfiniteCompositionsOfShape J W consists of those morphisms that are transfinite compositions of shape J using arrows in W.

Русский

Заданному W и хорошо упорядоченному типу J соответствует класс transfiniteCompositionsOfShape J W, состоящий из морфизмов, которые являются трансфинитными композициями формы J из стрелок в W.

LaTeX

$$$\\text{transfiniteCompositionsOfShape}(W,J) := \\{ f : X \\to Y \\mid \\exists t:\\, W.TransfiniteCompositionOfShape J f \\} $$$

Lean4

/-- Given `W : MorphismProperty C` and a well-ordered type `J`, this is
the class of morphisms that are transfinite composition of shape `J`
of morphisms in `W`. -/
def transfiniteCompositionsOfShape : MorphismProperty C := fun _ _ f ↦ Nonempty (W.TransfiniteCompositionOfShape J f)

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