theorem
MeasureTheory.Measure.ext_of_generateFrom_of_univ
{α : Type u_1}
{mα : MeasurableSpace α}
{C : Set (Set α)}
{μ ν : Measure α}
(hA : mα = MeasurableSpace.generateFrom C)
(hC : IsPiSystem C)
(h_univ : Set.univ ∈ C)
(hμ : μ Set.univ ≠ ⊤)
(h : ∀ s ∈ C, μ s = ν s)
:
theorem
MeasureTheory.ext_of_generateFrom_of_isProbabilityMeasure
{α : Type u_1}
{mα : MeasurableSpace α}
{C : Set (Set α)}
{μ ν : Measure α}
[IsProbabilityMeasure μ]
[IsProbabilityMeasure ν]
(hA : mα = MeasurableSpace.generateFrom C)
(hC : IsPiSystem C)
(hμν : ∀ s ∈ C, μ s = ν s)
: