ofMem — Mathlib

English

If a morphism f : X → Y satisfies W f, then f is a transfinite composition of shape Fin(2) consisting of arrows in W.

Русский

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

LaTeX

$$$\\exists Z,\\; a: X \\to Z,\\; b: Z \\to Y \\text{ with } W a \\\\land W b \\\\land a \\circ b = f$$$

Lean4

/-- If `f : X ⟶ Y` satisfies `W f`, then `f` is a transfinite composition of shape `Fin 2`
of morphisms in `W`. -/
def ofMem {X Y : C} (f : X ⟶ Y) (hf : W f) : W.TransfiniteCompositionOfShape (Fin 2) f :=
  ofComposableArrows W (.mk₁ f) (fun i ↦ by fin_cases i; assumption)

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