ProbabilityTheory.measure_compl_support

lemma measure_compl_support (μ : Measure S) [hμ : FiniteSupport μ] : μ μ.supportᶜ = 0 := by  let A := hμ.finite.choose  have : (μ.support : Set S)ᶜ ⊆ (A : Set S)ᶜ ∪ ⋃ x ∈ A.filter (μ {·} = 0), {x} := by    intro z hz    simp only [Measure.support, ne_eq, Finset.coe_filter, mem_compl_iff, mem_setOf_eq, not_and,      Decidable.not_not] at hz    by_cases h'z : z ∈ A    · simp [hz h'z, h'z]    · simp [h'z]  apply le_antisymm ?_ bot_le  calc μ (μ.support : Set S)ᶜ ≤ μ ((A : Set S)ᶜ ∪ ⋃ x ∈ A.filter (μ {·} = 0), {x}) :=    measure_mono this  _ ≤ μ (Aᶜ) + ∑ x ∈ A.filter (μ {·} = 0), μ {x} := by    apply (measure_union_le _ _).trans    gcongr    apply measure_biUnion_finset_le  _ ≤ 0 + ∑ x ∈ A.filter (μ {·} = 0), 0 := by    gcongr with x hx    · exact hμ.finite.choose_spec.le    · simp only [Finset.mem_filter] at hx      exact hx.2.le  _ = 0 := by simp