ofIsComplProd — Mathlib

English

The product-of-projections decomposition equals the full projection built from IsCompl.

Русский

Разложение через произведение проекций равно полной проекции, построенной из IsCompl.

LaTeX

$$$\mathrm{ofIsComplProd} h\; φ\; ψ = φ.paren{π} + ψ.paren{π}.$$$

Lean4

/-- The linear map from `(p →ₗ[R₁] F) × (q →ₗ[R₁] F)` to `E →ₗ[R₁] F`. -/
def ofIsComplProd {p q : Submodule R₁ E} (h : IsCompl p q) : (p →ₗ[R₁] F) × (q →ₗ[R₁] F) →ₗ[R₁] E →ₗ[R₁] F
    where
  toFun φ := ofIsCompl h φ.1 φ.2
  map_add' := by intro φ ψ; rw [Prod.snd_add, Prod.fst_add, ofIsCompl_add]
  map_smul' := by intro c φ; simp [Prod.smul_snd, Prod.smul_fst, ofIsCompl_smul]

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