map_starProjection' — Mathlib

English

A variant of the map_starProjection statement: map_starProjection' expresses the same transfer under an isometry.

Русский

Вариант выражения переноса через изометрию.

LaTeX

$$map_starProjection' (f) p x = map_starProjection (f) p x (formal equality).$$

Lean4

theorem _root_.LinearIsometry.map_starProjection' {E E' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E']
    [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 E'] (f : E →ₗᵢ[𝕜] E') (p : Submodule 𝕜 E) [p.HasOrthogonalProjection]
    [(p.map f).HasOrthogonalProjection] (x : E) : f (p.starProjection x) = (p.map f).starProjection (f x) :=
  have : (p.map f.toLinearMap).HasOrthogonalProjection := ‹_›
  f.map_starProjection p x

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