mkOfSucc_subinterval_eq — Mathlib

English

The composition of mkOfSucc with subinterval along a fixed i ∈ Fin l equals mkOfSucc of the endpoint j+i in Δ^n.

Русский

Сочетание mkOfSucc с подинтервалом даёт mkOfSucc на концевой индекс j+i в Δ^n.

LaTeX

$$$mkOfSucc\, i \circ \mathrm{subinterval}(j,l,h) = mkOfSucc\, \langle j+i.1, \dots \rangle$$$

Lean4

@[simp]
theorem mkOfSucc_subinterval_eq {n} (j l : ℕ) (hjl : j + l ≤ n) (i : Fin l) :
    mkOfSucc i ≫ subinterval j l hjl = mkOfSucc ⟨j + i.1, Nat.lt_of_lt_of_le (Nat.add_lt_add_left i.2 j) hjl⟩ :=
  by
  unfold subinterval mkOfSucc
  ext (i : Fin 2)
  match i with
  | 0 | 1 => simp; cutsat

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