diag_sub_val — Mathlib

English

For any TypeVec α of length n, composing subtypeVal applied to repeatEq α with diagSub yields the diagonal map prod.diag.

Русский

Для любого α типа TypeVec длины n композиция subtypeVal (repeatEq α) с diagSub даёт диагональное отображение prod.diag.

LaTeX

$$\operatorname{subtypeVal}(\operatorname{repeatEq}(\alpha)) \circ \operatorname{diagSub} = \operatorname{prod.diag}$$

Lean4

@[simp]
theorem diag_sub_val {n} {α : TypeVec.{u} n} : subtypeVal (repeatEq α) ⊚ diagSub = prod.diag :=
  by
  ext i x
  induction i with
  | fz => simp only [comp, subtypeVal, repeatEq.eq_2, diagSub, prod.diag]
  | fs _ i_ih => apply @i_ih (drop α)

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