mk₅_surjective — Mathlib

English

Every ComposableArrows C 5 is obtained from five objects X0,...,X5 and five arrows f0,...,f4 with X equal to mk5 f0 f1 f2 f3 f4.

Русский

Любой ComposableArrows C 5 получается из пяти объектов X0,...,X5 и пяти стрелок f0,...,f4 с X = mk5 f0 f1 f2 f3 f4.

LaTeX

$$$(X : ComposableArrows C 5)\;\Rightarrow\; \exists X_0,X_1,X_2,X_3,X_4,X_5 \;\exists f_0,f_1,f_2,f_3,f_4,\; X = mk_5 f_0 f_1 f_2 f_3 f_4$$$

Lean4

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

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