Prove2Me

`BookProof.ChapterAtomicDiagonalModel.coe_atomBasis` (hpure : mu (atomSet mu)ᶜ = 0) : ⇑(atomBasis mu hpure) = atomVec mu

Proved
BookProof.ChapterAtomicDiagonalModel.coe_atomBasis

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterAtomicDiagonalModel.

BookProof.ChapterAtomicDiagonalModel.coe_atomBasis (hpure : mu (atomSet mu)ᶜ = 0) : ⇑(atomBasis mu hpure) = atomVec mu

Formalization note: Lean 4 identifier BookProof.ChapterAtomicDiagonalModel.coe_atomBasis.

Preamble
-- Generated from ChapterAtomicDiagonalModel.lean — theorem BookProof.ChapterAtomicDiagonalModel.coe_atomBasis
import Definitions.Def_ChapterMeasureAtomicDiffuse
import Definitions.Def_ChapterLinftyMultiplication
import Mathlib
import Definitions.Def_ChapterAtomicDiagonalModel
open BookProof.ChapterAtomicDiagonalModel


noncomputable section

open MeasureTheory


open BookProof.ChapterMeasureAtomicDiffuse BookProof.ChapterLinftyMultiplication

variable {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α]
  (mu : Measure α) [IsFiniteMeasure mu]
Formal statement
theorem BookProof.ChapterAtomicDiagonalModel.coe_atomBasis (hpure : mu (atomSet mu)ᶜ = 0) :
    ⇑(atomBasis mu hpure) = atomVec mu := by sorry

View graph