The Lean 4 theorem `orthonormalEmbedding_norm_map` in the `ChapterH9` chapter of the timepiece formalization

Proved

BookProof.ChapterH9.orthonormalEmbedding_norm_map

by leonardopedro · Sep 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

timepiece

The Lean 4 theorem orthonormalEmbedding_norm_map in the ChapterH9 chapter of the timepiece formalization.

Preamble

-- Generated from ChapterH9.lean — theorem BookProof.ChapterH9.orthonormalEmbedding_norm_map
import Mathlib
import Definitions.Def_ChapterH9
open BookProof.ChapterH9


noncomputable section


open BookProof.ChapterH1 BookProof.ChapterH4 BookProof.ChapterH5 BookProof.ChapterH6
open BookProof.ChapterH8
open ContinuousLinearMap


variable {E F G : Type*}
  [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
  [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
  [NormedAddCommGroup G] [InnerProductSpace ℂ G] [CompleteSpace G]

Formal statement

theorem BookProof.ChapterH9.orthonormalEmbedding_norm_map {m : ℕ} (w : Fin m → E) (hw : Orthonormal ℂ w)
    (x : EuclideanSpace ℂ (Fin m)) : ‖orthonormalEmbedding w hw x‖ = ‖x‖ := by sorry

Source

https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterH9.lean

View graph