starProjection_bot — Mathlib

English

The adjoint (star) projection associated with the zero subspace is the zero map.

Русский

Звёздная проекция, соответствующая нулевому подпроизвольному подпространству, есть нулевой отображение.

LaTeX

$$$ (\perp : \mathrm{Submodule}_{\mathbb{K}} E).starProjection = 0 $$$

Lean4

@[simp]
theorem starProjection_bot : (⊥ : Submodule 𝕜 E).starProjection = 0 := by
  rw [starProjection, orthogonalProjection_bot, ContinuousLinearMap.comp_zero]

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