English
Let (φ_i) be a family of spaces indexed by I. Denote by proj_i the i-th coordinate projection from the Cartesian product ∏_{i∈I} φ_i to φ_i, and let π be the canonical map collecting all coordinate projections into a single map ∏_{i∈I} φ_i → ∏_{i∈I} φ_i. Then the composed map π ∘ proj equals the identity on ∏_{i∈I} φ_i.
Русский
Пусть имеется семейство пространств (φ_i), индексируемое множестом I. Обозначим проекцию на i-ю координату как proj_i: ∏_{i∈I} φ_i → φ_i, а пусть π — каноническое отображение, собирающее все проекции в одно отображение ∏_{i∈I} φ_i → ∏_{i∈I} φ_i. Тогда произведение π и proj равно тождественному отображению на ∏_{i∈I} φ_i.
LaTeX
$$$ \\pi\\,\\mathrm{proj} = \\mathrm{id}_{\\prod_{i\\in I} \\phi_i} $$$
Lean4
@[simp]
theorem pi_proj : pi proj = .id R (∀ i, φ i) :=
rfl
