subinterval — Mathlib

English

For fixed n and subinterval length l, there is a natural morphism from Δ^l to Δ^n associated to the subinterval [j, j+l] of Δ^n, for 0 ≤ j ≤ n−l.

Русский

Для фиксированного n и длины подинтервала l существует связанный с подинтервалом [j, j+l] переход Δ^l → Δ^n.

LaTeX

$$$\mathrm{subinterval}(n, j, l, h) : \Delta^l \to \Delta^n \quad (h: j+l \le n)$$$

Lean4

/-- The "inert" morphism associated to a subinterval `j ≤ i ≤ j + l` of `Fin (n + 1)`. -/
def subinterval {n} (j l : ℕ) (hjl : j + l ≤ n) : ⦋l⦌ ⟶ ⦋n⦌ :=
  SimplexCategory.mkHom
    { toFun := fun i => ⟨i.1 + j, (by cutsat)⟩
      monotone' := fun i i' hii' => by simpa only [Fin.mk_le_mk, add_le_add_iff_right] using hii' }

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