precomp_surjective — Mathlib

English

Every F ∈ ComposableArrows C (n+1) is a precomposition of some F₀ by some f₀.

Русский

Каждый F в ComposableArrows C (n+1) является предкомпозицией F₀ по некоторому f₀.

LaTeX

$$$$ \\exists F_0, X_0, f_0: X_0 \\to F_0.left \\; \\text{ s.t. } F = F_0.precomp f_0 $$$$

Lean4

theorem precomp_surjective (F : ComposableArrows C (n + 1)) :
    ∃ (F₀ : ComposableArrows C n) (X₀ : C) (f₀ : X₀ ⟶ F₀.left), F = F₀.precomp f₀ :=
  ⟨F.δ₀, _, F.map' 0 1, ext_succ rfl (by simp) (by simp)⟩

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