ofComp — Mathlib

English

If f : X → Y and g : Y → Z satisfy W f and W g, then f ≫ g is a transfinite composition of shape Fin(3) of arrows in W.

Русский

Если f : X → Y и g : Y → Z удовлетворяют W, то композиция f ≫ g является трансфинитной композицией формы Fin(3) стрел из W.

LaTeX

$$$\\exists X_1, X_2,\\; f_1: X \\to X_1,\\; f_2: X_1 \\to X_2,\\; f_3: X_2 \\to Z,\\; W f_1, W f_2, W f_3 \\land f_1 \\circ f_2 \\circ f_3 = f \\circ g$$$

Lean4

/-- If `f : X ⟶ Y` and `g : Y ⟶ Z` satisfy `W f` and `W g`, then `f ≫ g` is a
transfinite composition of shape `Fin 3` of morphisms in `W`. -/
def ofComp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : W f) (hg : W g) :
    W.TransfiniteCompositionOfShape (Fin 3) (f ≫ g) :=
  ofComposableArrows W (.mk₂ f g) (fun i ↦ by fin_cases i <;> assumption)

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