`BookProof.ChapterDeterministic.measOpSet_eq_sum` (U : Matrix (Fin n) (Fin n) ℂ) (B : Finset (Fin n)) : measOpSet U B = ∑ b ∈ B, measOp U b

Proved

BookProof.ChapterDeterministic.measOpSet_eq_sum

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterDeterministic.

BookProof.ChapterDeterministic.measOpSet_eq_sum (U : Matrix (Fin n) (Fin n) ℂ) (B : Finset (Fin n)) : measOpSet U B = ∑ b ∈ B, measOp U b

Formalization note: Lean 4 identifier BookProof.ChapterDeterministic.measOpSet_eq_sum.

Preamble

-- Generated from ChapterDeterministic.lean — theorem BookProof.ChapterDeterministic.measOpSet_eq_sum
import Definitions.Def_ChapterReconstruct
import Mathlib
import Definitions.Def_ChapterDeterministic
import Definitions.Def_ChapterElectroweakFieldStrength
import Definitions.Def_ChapterTimeTranslation
open BookProof.ChapterElectroweakFieldStrength
open BookProof.ChapterTimeTranslation
open BookProof.ChapterDeterministic


open scoped BigOperators
open Finset Matrix
open BookProof.ChapterReconstruct BookProof.ChapterTimeTranslation


variable {n : ℕ}

Formal statement

theorem BookProof.ChapterDeterministic.measOpSet_eq_sum (U : Matrix (Fin n) (Fin n) ℂ) (B : Finset (Fin n)) :
    measOpSet U B = ∑ b ∈ B, measOp U b := by sorry

View graph