const_subinterval_eq — Mathlib

English

The composition of the constant map into Δ^l and the subinterval map equals the constant map into Δ^n at the corresponding endpoint j+i.

Русский

Сведение константного отображения в Δ^l с отображением подинтервала даёт константное отображение в Δ^n на концы, соответствующие j+i.

LaTeX

$$$\Delta^0 .\text{const}_{\Delta^l}(i) \circ \mathrm{subinterval}(j,l,h) = \Delta^0 .\text{const}_{\Delta^n}(\langle j+i, \cdots \rangle)$$$

Lean4

theorem const_subinterval_eq {n} (j l : ℕ) (hjl : j + l ≤ n) (i : Fin (l + 1)) :
    ⦋0⦌.const ⦋l⦌ i ≫ subinterval j l hjl =
      ⦋0⦌.const ⦋n⦌ ⟨j + i.1, lt_add_of_lt_add_right (Nat.add_lt_add_left i.2 j) hjl⟩ :=
  by
  rw [const_comp]
  congr
  ext
  dsimp [subinterval]
  rw [add_comm]

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