ker_orthogonalProjection — Mathlib

English

The kernel of the orthogonal projection equals the orthogonal complement: ker K.orthogonalProjection = K^⊥.

Русский

Ядро ортогональной проекции равно ортогональному дополнению: ker K.orthogonalProjection = K^⊥.

LaTeX

$$ker(K.orthogonalProjection) = K^{\perp}.$$

Lean4

@[simp]
theorem ker_orthogonalProjection : LinearMap.ker K.orthogonalProjection = Kᗮ := by ext;
  exact orthogonalProjection_eq_zero_iff

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