instHasOrthogonalProjectionTop — Mathlib

English

The top subspace ⊤ of E admits an orthogonal projection onto itself, trivially given by the identity inclusion.

Русский

Верхнее подпространство ⊤ пространства E обладает ортогональной проекцией на себя, тривиально заданной тождественным включением.

LaTeX

$$⊤ HasOrthogonalProjection$$

Lean4

instance : (⊤ : Submodule 𝕜 E).HasOrthogonalProjection :=
  ⟨fun v ↦ ⟨v, trivial, by simp⟩⟩

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