Prove2Me

`BookProof.ChapterUnitaryTransport.transport_isSelfAdjointOn` (W : H ≃ₗᵢ[ℂ] K) (D : Submodule ℂ H) (A : D →ₗ[ℂ] H) (hA : IsSelfAdjointOn D A) : IsSelfAdjointOn (transportDomain W D

Proved
BookProof.ChapterUnitaryTransport.transport_isSelfAdjointOn

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterUnitaryTransport.

BookProof.ChapterUnitaryTransport.transport_isSelfAdjointOn (W : H ≃ₗᵢ[ℂ] K) (D : Submodule ℂ H) (A : D →ₗ[ℂ] H) (hA : IsSelfAdjointOn D A) : IsSelfAdjointOn (transportDomain W D) (transportOp W D A)

Formalization note: Lean 4 identifier BookProof.ChapterUnitaryTransport.transport_isSelfAdjointOn.

Preamble
-- Generated from ChapterUnitaryTransport.lean — theorem BookProof.ChapterUnitaryTransport.transport_isSelfAdjointOn
import Mathlib
import Definitions.Def_ChapterUnitaryTransport
import Definitions.Def_ChapterUnboundedPosition
open BookProof.ChapterUnboundedPosition
open BookProof.ChapterUnitaryTransport


open scoped InnerProductSpace


variable {H K : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [NormedAddCommGroup K] [InnerProductSpace ℂ K]
Formal statement
theorem BookProof.ChapterUnitaryTransport.transport_isSelfAdjointOn (W : H ≃ₗᵢ[ℂ] K) (D : Submodule ℂ H) (A : D →ₗ[ℂ] H)
    (hA : IsSelfAdjointOn D A) :
    IsSelfAdjointOn (transportDomain W D) (transportOp W D A) := by sorry

View graph