`BookProof.ChapterPvmMeasure.Pvm.add_of_disjoint` {E F : Set X} (hE : MeasurableSet E) (hF : MeasurableSet F) (hd : Disjoint E F) (u : H) : P.p (E ∪ F) u = P.p E u + P.p F u

Initializing...

`BookProof.ChapterPvmMeasure.Pvm.add_of_disjoint` {E F : Set X} (hE : MeasurableSet E) (hF : MeasurableSet F) (hd : Disjoint E F) (u : H) : P.p (E ∪ F) u = P.p E u + P.p F u · Prove2Me