`BookProof.ClosureUniqueness.positive_sqrt_unique` {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S B C : H →L[ℂ] H) (hB : B.IsPositive) (hC : C.IsPo

Proved

BookProof.ClosureUniqueness.positive_sqrt_unique

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterClosureUniqueness.

BookProof.ClosureUniqueness.positive_sqrt_unique {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S B C : H →L[ℂ] H) (hB : B.IsPositive) (hC : C.IsPositive) (hBS : B ∘L B = S) (hCS : C ∘L C = S) : B = C

Formalization note: Lean 4 identifier BookProof.ClosureUniqueness.positive_sqrt_unique.

Preamble

-- Generated from ChapterClosureUniqueness.lean — theorem BookProof.ClosureUniqueness.positive_sqrt_unique
import Definitions.Def_ChapterFarisLavine
import Definitions.Def_ChapterEsaClosureCore
import Mathlib
import Definitions.Def_ChapterClosureUniqueness
open BookProof.ClosureUniqueness



open BookProof.FarisLavine BookProof.EsaClosure

variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]
variable {D D₁ D₂ Dom Dom₁ Dom₂ : Submodule ℂ F}

variable [CompleteSpace F]

Formal statement

theorem BookProof.ClosureUniqueness.positive_sqrt_unique {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
    [CompleteSpace H] (S B C : H →L[ℂ] H) (hB : B.IsPositive) (hC : C.IsPositive)
    (hBS : B ∘L B = S) (hCS : C ∘L C = S) : B = C := by sorry

View graph