norm_starProjection_apply_le — Mathlib

English

The star projection is also nonexpanding: the norm of starProjection(v) is ≤ ||v|| for all v.

Русский

Звёздная проекция также нерасширяет норму: для любого v выполняется ||K.starProjection(v)|| ≤ ||v||.

LaTeX

$$$ \|K.starProjection(v)\| \leq \|v\| \quad \text{for all } v \in E $$$

Lean4

theorem norm_starProjection_apply_le (v : E) : ‖K.starProjection v‖ ≤ ‖v‖ :=
  K.norm_orthogonalProjection_apply_le v

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