single_eq_pi_diag — Mathlib

English

For each i, the i-th canonical injection into the Pi-type, denoted single R φ i, is equal to the Pi-diagonal map pi applied to diag i; i.e., single R φ i = π(diag i).

Русский

Для каждого i каноническое внедрение в произведение функций одинаково с отображением диагонали: single R φ i = π(diag i).

LaTeX

$$$$\\text{single}_{R,\\varphi}(i) = \\pi(\\text{diag}_i).$$$$

Lean4

theorem single_eq_pi_diag (i : ι) : single R φ i = pi (diag i) :=
  by
  ext x j
  convert (update_apply 0 x i j _).symm
  rfl

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