mk₃_surjective — Mathlib

English

For any X ∈ ComposableArrows C 3 there exist X0,X1,X2,X3 and f0,f1,f2 with X = mk₃ f0 f1 f2.

Русский

Для любого X ∈ ComposableArrows C 3 существуют X0,X1,X2,X3 и переходы f0,f1,f2 такие, что X = mk₃ f0 f1 f2.

LaTeX

$$$\\forall X:\\, \\text{ComposableArrows}~C~3,\\; \\exists X_0,X_1,X_2,X_3\\exists f_0:f_0\\to f_1\\exists f_1:f_1\\to f_2\\exists f_2:f_2\\to X_3, \\; X = mk_3 f_0 f_1 f_2$$$

Lean4

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

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