eq_starProjection_of_eq_submodule

English

If K = K', then the star projections coincide: P_K = P_{K'}.

Русский

Если K = K', то P_K = P_{K'}.

LaTeX

$$K = K' \Rightarrow P_K = P_{K'}.$$

Lean4

/-- The orthogonal projections onto equal subspaces are coerced back to the same point in `E`. -/
@[deprecated "As there are no subtypes causing dependent type issues, there is no need for this
      result as `simp` will suffice" (since := "12-07-2025")]
theorem eq_starProjection_of_eq_submodule {K' : Submodule 𝕜 E} [K'.HasOrthogonalProjection] (h : K = K') (u : E) :
    K.starProjection u = K'.starProjection u := by simp [h]

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