norm_orthogonalProjection_apply — Mathlib

English

If v lies in K, the orthogonal projection of v onto K has the same norm as v.

Русский

Если вектор v принадлежит K, нормa ортогональной проекции v на K равна norm v.

LaTeX

$$$ \|\mathrm{orthogonalProjection}_K(v)\| = \|v\| \quad \text{for } v \in K $$$

Lean4

theorem norm_orthogonalProjection_apply {v : E} (hv : v ∈ K) : ‖orthogonalProjection K v‖ = ‖v‖ :=
  congr(‖$(K.starProjection_eq_self_iff.mpr hv)‖)

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