English
For every n and i, the 0-face of the horn Λ^{n+2}_{i} evaluates to the top element (i.e., the whole set).
Русский
Для любых n и i вершина 0 норна Λ^{n+2}_{i} равна верхнему элементу (то есть всему множеству).
LaTeX
$$$ (\mathrm{horn}(n+2,i)).obj(\op (.mk 0)) = \top $$$
Lean4
@[simp]
theorem horn_obj_zero (n : ℕ) (i : Fin (n + 3)) : (horn.{u} (n + 2) i).obj (op (.mk 0)) = ⊤ :=
by
ext j
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, Finset.mem_compl, Finset.mem_singleton, exists_prop,
Set.top_eq_univ, Set.mem_univ, iff_true]
let S : Finset (Fin (n + 3)) := {i, j 0}
have hS : ¬(S = Finset.univ) := fun hS ↦
by
have := Finset.card_le_card hS.symm.le
simp only [Finset.card_univ, Fintype.card_fin, S] at this
have := this.trans Finset.card_le_two
cutsat
rw [Finset.eq_univ_iff_forall, not_forall] at hS
obtain ⟨k, hk⟩ := hS
simp only [Finset.mem_insert, Finset.mem_singleton, not_or, S] at hk
refine ⟨k, hk.1, fun a ↦ ?_⟩
fin_cases a
exact Ne.symm hk.2
