English
For subcomplexes A ≤ B, A ≤ B iff every non-degenerate simplex of A lies in B.
Русский
Для Подкомплекс A ≤ B, верно A ≤ B тогда и только тогда, когда каждая недегенеративная симплекса A принадлежит B.
LaTeX
$$$ A \le B \;\Longleftrightarrow\; \forall n, x \in X_{\text{nonDegenerate}}(n), x \in A.obj(\cdot) \Rightarrow x \in B.obj(\cdot) $$$
Lean4
theorem mem_degenerate_iff {n : ℕ} (x : A.obj (op ⦋n⦌)) : x ∈ degenerate A n ↔ x.val ∈ X.degenerate n :=
by
rw [SSet.mem_degenerate_iff, SSet.mem_degenerate_iff]
constructor
· rintro ⟨m, hm, f, _, y, rfl⟩
exact ⟨m, hm, f, inferInstance, y.val, rfl⟩
· obtain ⟨x, hx⟩ := x
rintro ⟨m, hm, f, _, ⟨y, rfl⟩⟩
refine ⟨m, hm, f, inferInstance, ⟨y, ?_⟩, rfl⟩
have := isSplitEpi_of_epi f
simpa [Set.mem_preimage, ← op_comp, ← FunctorToTypes.map_comp_apply, IsSplitEpi.id, op_id,
FunctorToTypes.map_id_apply] using A.map (section_ f).op hx
