Restriction of the unitary is the unitary

Proved

BookProof.ChapterUnitaryTransport.transportEquiv_coe

by hitme development · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

spectral-theorytimepiece

The restriction of a unitary $W$ to a subspace $D$ is still $W$ on vectors of $D$ .

(W|_D)(x) = Wx \qquad (x\in D).

Formalization Note. transportEquiv is submoduleMap of $W$ .

Preamble

import Mathlib
import Definitions.Def_ChapterUnitaryTransport
open BookProof.ChapterUnitaryTransport
open scoped InnerProductSpace

Formal statement

theorem BookProof.ChapterUnitaryTransport.transportEquiv_coe {H K : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [NormedAddCommGroup K] [InnerProductSpace ℂ K] (W : H ≃ₗᵢ[ℂ] K) (D : Submodule ℂ H) (x : D) : ((transportEquiv W D x : transportDomain W D) : K) = W (x : H) := by sorry

Source

timepiece BookProof, ChapterUnitaryTransport.lean, theorem transportEquiv_coe

View graph