Unitaries send dense domains to dense domains

Proved

BookProof.ChapterUnitaryTransport.transportDomain_dense

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

spectral-theorytimepiece

If $D\subseteq H$ is dense and $W:H\to K$ is unitary, then $W(D)$ is dense in $K$ .

\overline{D}=H \quad\Longrightarrow\quad \overline{W(D)}=K.

Formalization Note. $W$ is a homeomorphism, hence a dense embedding.

Preamble

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

Formal statement

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

Source

timepiece BookProof, ChapterUnitaryTransport.lean, theorem transportDomain_dense

View graph