Prove2Me

`BookProof.DirectSumEsa.dsOp_symmetricOn` (H : ∀ i, D i →ₗ[ℂ] G i) (hsym : ∀ i, SymmetricOn (D i) (H i)) : SymmetricOn (dsCore D) (dsOp H)

Proved
BookProof.DirectSumEsa.dsOp_symmetricOn

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterDirectSumEsa.

BookProof.DirectSumEsa.dsOp_symmetricOn (H : ∀ i, D i →ₗ[ℂ] G i) (hsym : ∀ i, SymmetricOn (D i) (H i)) : SymmetricOn (dsCore D) (dsOp H)

Formalization note: Lean 4 identifier BookProof.DirectSumEsa.dsOp_symmetricOn.

Preamble
-- Generated from ChapterDirectSumEsa.lean — theorem BookProof.DirectSumEsa.dsOp_symmetricOn
import Definitions.Def_ChapterFarisLavine
import Mathlib
import Definitions.Def_ChapterDirectSumEsa
import Definitions.Def_ChapterFarisLavineCore
open BookProof.DirectSumEsa


open scoped ENNReal


open BookProof.FarisLavine

noncomputable section

variable {ι : Type*} {G : ι → Type*} [∀ i, NormedAddCommGroup (G i)]
  [∀ i, InnerProductSpace ℂ (G i)]

variable {D : ∀ i, Submodule ℂ (G i)}
Formal statement
theorem BookProof.DirectSumEsa.dsOp_symmetricOn (H : ∀ i, D i →ₗ[ℂ] G i) (hsym : ∀ i, SymmetricOn (D i) (H i)) :
    SymmetricOn (dsCore D) (dsOp H) := by sorry

View graph