intervalEdge — Mathlib

English

The morphism intervalEdge(n, j, l, h) : Δ^1 → Δ^n selects the edge spanning the interval from j to j+l in Δ^n, with j+l ≤ n.

Русский

Морфизм intervalEdge(n, j, l, h): Δ^1 → Δ^n выбирает ребро, охватывающее интервал от j до j+l в Δ^n, при условии j+l ≤ n.

LaTeX

$$$\mathrm{intervalEdge}(n, j, l, h) : \Delta^1 \to \Delta^n$$$

Lean4

/-- The morphism `⦋1⦌ ⟶ ⦋n⦌` that picks out the edge spanning the interval from `j` to `j + l`. -/
def intervalEdge {n} (j l : ℕ) (hjl : j + l ≤ n) : ⦋1⦌ ⟶ ⦋n⦌ :=
  mkOfLe ⟨j, (by cutsat)⟩ ⟨j + l, (by cutsat)⟩ (Nat.le_add_right j l)

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