pi_proj_comp — Mathlib

English

Let f be a continuous linear map from M₂ to ∏_{i} φ_i. Then assembling the coordinate projections after f yields f itself: π (proj ∘_L f) = f.

Русский

Пусть f — непрерывное линейное отображение M₂ в произведение ∏_{i} φ_i. Тогда, применив проекции к f и собрав их обратно, получаем то же отображение: π (proj ∘_L f) = f.

LaTeX

$$$ \\pi\\big( \\mathrm{proj} \\circ_L f \\big) = f $$$

Lean4

@[simp]
theorem pi_proj_comp (f : M₂ →L[R] ∀ i, φ i) : pi (proj · ∘L f) = f :=
  rfl

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