primitiveTriangle — Mathlib

English

The primitiveTriangle furnishes the 2-dimensional face (a triangle) inside the horn Λ[n+3,i], with vertices k, k+1, k+2, under various index inequalities.

Русский

primitiveTriangle строит треугольник внутри горна Λ[n+3,i] со вершинами k, k+1, k+2 при различных неравенствах индексов.

LaTeX

$$$\mathrm{primitiveTriangle} : {n,i,k} \to (\Lambda[n+3,i]).⦋2⦌ $$$

Lean4

/-- The triangle in the standard simplex with vertices `k`, `k+1`, and `k+2`.

This constructor assumes `0 < i < n`,
which is the type of horn that occurs in the horn-filling condition of quasicategories. -/
@[simps]
def primitiveTriangle {n : ℕ} (i : Fin (n + 4)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 3)) (k : ℕ) (h : k < n + 2) :
    (Λ[n + 3, i] : SSet.{u}) _⦋2⦌ :=
  by
  refine ⟨stdSimplex.triangle (n := n + 3) ⟨k, by cutsat⟩ ⟨k + 1, by cutsat⟩ ⟨k + 2, by cutsat⟩ ?_ ?_, ?_⟩
  · simp only [Fin.mk_le_mk, le_add_iff_nonneg_right, zero_le]
  ·
    simp only [Fin.mk_le_mk, add_le_add_iff_left, one_le_two]
      -- this was produced using `simp? [horn_eq_iSup]`

  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]
  have hS :
    ¬({i, (⟨k, by cutsat⟩ : Fin (n + 4)), (⟨k + 1, by cutsat⟩ : Fin (n + 4)), (⟨k + 2, by cutsat⟩ : Fin (n + 4))} =
        Finset.univ) :=
    fun hS ↦ by
    obtain ⟨i, hi⟩ := i
    by_cases hk : k = 0
    · subst hk
      have := Finset.mem_univ (Fin.last _ : Fin (n + 4))
      rw [← hS] at this
      simp only [Fin.zero_eta, zero_add, Fin.mk_one, mem_insert, Fin.ext_iff, Fin.val_last, Fin.val_zero,
        AddLeftCancelMonoid.add_eq_zero, OfNat.ofNat_ne_zero, and_false, Fin.val_one, Nat.reduceEqDiff, mem_singleton,
        or_self, or_false] at this
      simp only [Fin.lt_iff_val_lt_val, Fin.val_last] at hₙ
      cutsat
    · have := Finset.mem_univ (0 : Fin (n + 4))
      rw [← hS] at this
      simp only [mem_insert, Fin.ext_iff, Fin.val_zero, right_eq_add, AddLeftCancelMonoid.add_eq_zero, one_ne_zero,
        and_false, mem_singleton, OfNat.ofNat_ne_zero, or_self, or_false] at this
      obtain rfl | rfl := this <;> tauto
  rw [Finset.eq_univ_iff_forall, not_forall] at hS
  obtain ⟨l, hl⟩ := hS
  simp only [mem_insert, mem_singleton, not_or] at hl
  refine ⟨l, hl.1, fun a ↦ ?_⟩
  fin_cases a
  · exact Ne.symm hl.2.1
  · exact Ne.symm hl.2.2.1
  · exact Ne.symm hl.2.2.2

Похожие утверждения