proj_comp_single — Mathlib

English

The composition of the i-th projection with the j-th injection equals the diagonal map: (proj i) ∘ (single R φ j) = diag j i.

Русский

Составление проекции i с внедрением j даёт диагональное отображение: (proj i) ∘ (single R φ j) = diag j i.

LaTeX

$$$$\\bigl(\\mathrm{proj}_i\\bigr)\\circ \\bigl(\\text{single}_{R,\\varphi}(j)\\bigr) = \\text{diag}_{j i}.$$$$

Lean4

theorem proj_comp_single (i j : ι) : (proj i).comp (single R φ j) = diag j i := by rw [single_eq_pi_diag, proj_pi]

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