Transported domain is the unitary image

Proved

BookProof.ChapterUnitaryTransport.coe_transportDomain

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

spectral-theorytimepiece

The transported domain $W(D)$ is, as a set, exactly the image of $D$ under the unitary $W$ .

W(D) = \{ Wx : x\in D \}.

Formalization Note. transportDomain is Submodule.map of $W$ .

Preamble

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

Formal statement

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

Source

timepiece BookProof, ChapterUnitaryTransport.lean, theorem coe_transportDomain

View graph