English
Every x in X_n arises as X.map f.op y for some non-degenerate y and epimorphic f, possibly after iterating.
Русский
Каждый x в X_n можно представить как X.map f.op y для некоторого недегенеративного y и эпиморфного f, возможно по итерациям.
LaTeX
$$$ \exists m, \exists f: [n] \to [m], \text{ epi } f, \exists y \in X_{\text{nonDegenerate}}(m), x = X.map f^{op} y $$$
Lean4
theorem exists_nonDegenerate (x : X _⦋n⦌) :
∃ (m : ℕ) (f : ⦋n⦌ ⟶ ⦋m⦌) (_ : Epi f) (y : X.nonDegenerate m), x = X.map f.op y := by
induction n with
| zero => exact ⟨0, 𝟙 _, inferInstance, ⟨x, by simp⟩, by simp⟩
| succ n hn =>
by_cases hx : x ∈ X.nonDegenerate (n + 1)
· exact ⟨n + 1, 𝟙 _, inferInstance, ⟨x, hx⟩, by simp⟩
· simp only [← mem_degenerate_iff_notMem_nonDegenerate, degenerate_eq_iUnion_range_σ, Set.mem_iUnion,
Set.mem_range] at hx
obtain ⟨i, y, rfl⟩ := hx
obtain ⟨m, f, hf, z, rfl⟩ := hn y
exact ⟨_, SimplexCategory.σ i ≫ f, inferInstance, z, by simp; rfl⟩
