English
An induction principle for HigherFacesVanish that reduces the verification to the base case δ₀ when a certain set of maps are δ-maps. It shows vanishing persists under the standard δ-structure.
Русский
Принцип индукции для HigherFacesVanish, который сводит проверку к базовому случаю δ₀, когда набор отображений является δ-маршрутом. Показывает, что исчезновение сохраняется при стандартной δ-структуре.
LaTeX
$$$\text{If } v: \text{HigherFacesVanish}_q,\text{ then } v \text{ persists under } δ_0$ in the appropriate indexing.$$
Lean4
theorem iff {j : ℕ} {i : Fin (j + 2)} : Isδ₀ (SimplexCategory.δ i) ↔ i = 0 :=
by
constructor
· rintro ⟨_, h₂⟩
by_contra h
exact h₂ (Fin.succAbove_ne_zero_zero h)
· rintro rfl
exact ⟨rfl, by dsimp; exact Fin.succ_ne_zero (0 : Fin (j + 1))⟩
