English
The edge of the horn Λ[n,i] with endpoints a and b exists when {i,a,b} has cardinality at most n, giving an edge object.
Русский
Ребро горна Λ[n,i] с конечными точками a и b существует тогда, когда множество {i,a,b} имеет кардинал равный или меньше n.
LaTeX
$$$ (\mathrm{horn}\; n\; i).toSSet.obj{\ unop := \mathrm{SimplexCategory.mk} 1 } $$$
Lean4
/-- The edge of `Λ[n, i]` with endpoints `a` and `b`.
This edge only exists if `{i, a, b}` has cardinality less than `n`. -/
@[simps]
def edge (n : ℕ) (i a b : Fin (n + 1)) (hab : a ≤ b) (H : #{ i, a, b } ≤ n) : (Λ[n, i] : SSet.{u}) _⦋1⦌ :=
⟨stdSimplex.edge n a b hab,
by
have hS : ¬({ i, a, b } = Finset.univ) := fun hS ↦
by
have := Finset.card_le_card hS.symm.le
simp only [card_univ, Fintype.card_fin] at this
cutsat
rw [Finset.eq_univ_iff_forall, not_forall] at hS
obtain ⟨k, hk⟩ := hS
simp only [mem_insert, mem_singleton, not_or] at hk
simp only [horn_eq_iSup, Subpresheaf.iSup_obj, Set.iUnion_coe_set, Set.mem_compl_iff, Set.mem_singleton_iff,
Set.mem_iUnion, stdSimplex.mem_face_iff, Nat.reduceAdd, mem_compl, mem_singleton, exists_prop]
refine ⟨k, hk.1, fun a ↦ ?_⟩
fin_cases a
· exact Ne.symm hk.2.1
· exact Ne.symm hk.2.2⟩
