fst_diag — Mathlib

English

The left projection composed with the diagonal equals the identity: fst ∘ diag = id.

Русский

Левая проекция, составленная с диагонализацией, равна тождественному отображению: fst ∘ diag = id.

LaTeX

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

Lean4

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

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