`BookProof.NavierStokesFlow.FullEsa.IsSymmetricDom.sum` {ι : Type*} (s : Finset ι) {A : ι → (D →ₗ[ℂ] D)} (hA : ∀ i ∈ s, IsSymmetricDom (A i)) : IsSymmetricDom (∑ i ∈ s, A i)
ProvedBookProof.NavierStokesFlow.FullEsa.IsSymmetricDom.sumtheoremstimepiece
Prove the following Lean 4 theorem from ChapterNavierStokesFullEsa.
BookProof.NavierStokesFlow.FullEsa.IsSymmetricDom.sum {ι : Type*} (s : Finset ι) {A : ι → (D →ₗ[ℂ] D)} (hA : ∀ i ∈ s, IsSymmetricDom (A i)) : IsSymmetricDom (∑ i ∈ s, A i)
Formalization note: Lean 4 identifier BookProof.NavierStokesFlow.FullEsa.IsSymmetricDom.sum.
Preamble
-- Generated from ChapterNavierStokesFullEsa.lean — theorem BookProof.NavierStokesFlow.FullEsa.IsSymmetricDom.sum
import Mathlib
import Definitions.Def_ChapterNavierStokesFullEsa
import Definitions.Def_ChapterSirkFinitePrecision
import Definitions.Def_ChapterNavierStokesAffineFiberEsa
open BookProof.SirkFinitePrecision
open BookProof.SirkFinitePrecision.CertInterval
open BookProof.NavierStokesFlow
open scoped ENNReal
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]
variable {D : Submodule ℂ F}Formal statement
theorem BookProof.NavierStokesFlow.FullEsa.IsSymmetricDom.sum {ι : Type*} (s : Finset ι) {A : ι → (D →ₗ[ℂ] D)}
(hA : ∀ i ∈ s, IsSymmetricDom (A i)) : IsSymmetricDom (∑ i ∈ s, A i) := by sorry