triangle — Mathlib

English

The triangle in Δ[n] with vertices a ≤ b ≤ c is the 2-dimensional face determined by these vertices.

Русский

Треугольник в Δ[n] с вершинами a ≤ b ≤ c есть 2-мерная грань, заданная этими вершинами.

LaTeX

$$triangle {n} (a,b,c) (hab : a ≤ b) (hbc : b ≤ c) : Δ[n]_{⟨2⟩}$$

Lean4

/-- The triangle in the standard simplex with vertices `a`, `b`, and `c`. -/
def triangle {n : ℕ} (a b c : Fin (n + 1)) (hab : a ≤ b) (hbc : b ≤ c) : Δ[n] _⦋2⦌ :=
  by
  refine objMk ⟨![a, b, c], ?_⟩
  rw [Fin.monotone_iff_le_succ]
  simp only [unop_op, len_mk, Fin.forall_fin_two]
  dsimp
  simp only [*, true_and]

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