mk₂_surjective — Mathlib

English

Every 2-length composable arrow X arises as mk₂ of its two edge maps X.map' 0 1 and X.map' 1 2 with the obvious domain/codomain objects and arrows.

Русский

Любой 2‑ступенчатый композиционный стрел X можно представить как mk₂ f0 f1, где f0 = X.map'0 1 и f1 = X.map'1 2.

LaTeX

$$$\\exists X_0,X_1,X_2\\ (\\text{f}_0:X_0\\to X_1)\\ (\\text{f}_1:X_1\\to X_2),\\ X = mk_2 f_0 f_1$$$

Lean4

theorem mk₂_surjective (X : ComposableArrows C 2) : ∃ (X₀ X₁ X₂ : C) (f₀ : X₀ ⟶ X₁) (f₁ : X₁ ⟶ X₂), X = mk₂ f₀ f₁ :=
  ⟨_, _, _, X.map' 0 1, X.map' 1 2, ext₂ rfl rfl rfl (by simp) (by simp)⟩

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