edge — Mathlib

English

The edge of Δ[n] with endpoints a and b (a ≤ b) is the 1-dimensional face determined by those endpoints.

Русский

Ребро Δ[n] с концами a и b (a ≤ b) есть 1-мерная грань, задаваемая этими концами.

LaTeX

$$$edge(n,a,b,hab) : \\Delta[n]_{⟨1⟩}$ is the 1-simplex with endpoints $a$ and $b$.$$

Lean4

/-- The edge of the standard simplex with endpoints `a` and `b`. -/
def edge (n : ℕ) (a b : Fin (n + 1)) (hab : a ≤ b) : Δ[n] _⦋1⦌ :=
  by
  refine objMk ⟨![a, b], ?_⟩
  rw [Fin.monotone_iff_le_succ]
  simp only [unop_op, len_mk, Fin.forall_fin_one]
  apply Fin.mk_le_mk.mpr hab

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