mem_iff_norm_starProjection — Mathlib

English

For a subspace U with an orthogonal projection, v ∈ U if and only if ||U.starProjection v|| = ||v||.

Русский

Для подпространства U с ортогональной проекцией верно: v ∈ U тогда и только тогда, когда ||U.starProjection v|| = ||v||.

LaTeX

$$$ v \in U \iff \|U.starProjection(v)\| = \|v\|. $$$

Lean4

theorem mem_iff_norm_starProjection (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (v : E) :
    v ∈ U ↔ ‖U.starProjection v‖ = ‖v‖ :=
  by
  refine ⟨fun h => norm_starProjection_apply _ h, fun h => ?_⟩
  simpa [h, sub_eq_zero, eq_comm (a := v), starProjection_eq_self_iff] using U.norm_sq_eq_add_norm_sq_starProjection v

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