snd_diag — Mathlib

English

Similarly, snd ∘ diag = id, i.e., the right projection after diagonalization returns the original vector.

Русский

Аналогично, snd ∘ diag = id; правая проекция после диагонализации возвращает исходный вектор.

LaTeX

$$$\\mathrm{snd} \\circ \\mathrm{diag} = \\mathrm{id}$$$

Lean4

theorem snd_diag {α : TypeVec n} : TypeVec.prod.snd ⊚ (prod.diag : α ⟹ _) = id := by funext i;
  induction i with
  | fz => rfl
  | fs _ i_ih => apply i_ih

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