eq_comp_δ_of_not_surjective — Mathlib

English

If θ: Δ ⟶ ⦋n+1⦧ is not surjective, there exists i and θ' with θ = θ' ∘ δ_i.

Русский

Если θ: Δ ⟶ ⦋n+1⦧ не сюръективен, то существует i и θ' такие что θ = θ' ∘ δ_i.

LaTeX

$$$\\\\exists i \\\\in \\\\mathrm{Fin}(n+2),\\\\exists θ': Δ \\\\to ⦋n⦧,\\\\ θ = θ' \\\\circ δ i$$$

Lean4

theorem eq_comp_δ_of_not_surjective {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ ⦋n + 1⦌)
    (hθ : ¬Function.Surjective θ.toOrderHom) : ∃ (i : Fin (n + 2)) (θ' : Δ ⟶ ⦋n⦌), θ = θ' ≫ δ i :=
  by
  obtain ⟨i, hi⟩ := not_forall.mp hθ
  use i
  exact eq_comp_δ_of_not_surjective' θ i (not_exists.mp hi)

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