English
The primitiveEdge constructor yields the edge between vertices j and j+1 in the horn Λ[n,i], under suitable inequalities ensuring the edge is valid.
Русский
Конструктор primitiveEdge задаёт ребро между вершинами j и j+1 в горне Λ[n,i], при соблюдении соответствующих неравенств.
LaTeX
$$$\mathrm{primitiveEdge} : {n,i,j} \to (\Lambda[n,i]).⦋1⦌ $$$
Lean4
/-- The edge of `Λ[n, i]` with endpoints `j` and `j+1`.
This constructor assumes `0 < i < n`,
which is the type of horn that occurs in the horn-filling condition of quasicategories. -/
@[simps!]
def primitiveEdge {n : ℕ} {i : Fin (n + 1)} (h₀ : 0 < i) (hₙ : i < Fin.last n) (j : Fin n) :
(Λ[n, i] : SSet.{u}) _⦋1⦌ := by
refine edge n i j.castSucc j.succ ?_ ?_
· simp only [← Fin.val_fin_le, Fin.coe_castSucc, Fin.val_succ, le_add_iff_nonneg_right, zero_le]
simp only [← Fin.val_fin_lt, Fin.val_zero, Fin.val_last] at h₀ hₙ
obtain rfl | hn : n = 2 ∨ 2 < n := by rw [eq_comm, or_comm, ← le_iff_lt_or_eq]; cutsat
· revert i j; decide
· exact Finset.card_le_three.trans hn
