hasOrthogonalProjection_range — Mathlib

English

Let p be a symmetric projection on an inner product space. Then the subspace range(p) admits an orthogonal projection onto itself.

Русский

Пусть p — симметричная проекция на пространстве с скалярным произведением. Тогда подпространство range(p) имеет ортогональную проекцию на саму себя.

LaTeX

$$$ \exists Q: E \to E,\ Q^2 = Q,\ Q^* = Q,\ \operatorname{Im}(Q) = \operatorname{range}(p). $$$

Lean4

theorem _root_.LinearMap.IsSymmetricProjection.hasOrthogonalProjection_range {p : E →ₗ[𝕜] E}
    (hp : p.IsSymmetricProjection) : (range p).HasOrthogonalProjection :=
  ⟨fun v =>
    ⟨p v, by
      simp [hp.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hp.isSymmetric, ← Module.End.mul_apply,
        hp.isIdempotentElem.eq]⟩⟩

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