LeanMachineLearning exposition

1.4. ForMathlib.MeasureTheory.OuterMeasure.Basic🔗

Lemma about measures that assign non-zero probability to every singleton.

Module LeanMachineLearning.ForMathlib.MeasureTheory.OuterMeasure.Basic contains 1 exposed declarations.

measure_null_iff_eq_empty_of_measure_singleton_ne_zero🔗

LemmaMeasureTheory.measure_null_iff_eq_empty_of_measure_singleton_ne_zero
Details

No docstring.

🔗theorem
MeasureTheory.measure_null_iff_eq_empty_of_measure_singleton_ne_zero.{u_1,
    u_2}
  {α : Type u_1} {F : Type u_2} [FunLike F (Set α) ENNReal]
  [OuterMeasureClass F α] {μ : F} {s : Set α}
  (h : ∀ (a : α), μ {a} ≠ 0) : μ s = 0 ↔ s = ∅
MeasureTheory.measure_null_iff_eq_empty_of_measure_singleton_ne_zero.{u_1,
    u_2}
  {α : Type u_1} {F : Type u_2}
  [FunLike F (Set α) ENNReal]
  [OuterMeasureClass F α] {μ : F}
  {s : Set α} (h : ∀ (a : α), μ {a} ≠ 0) :
  μ s = 0 ↔ s = ∅

Code

lemma measure_null_iff_eq_empty_of_measure_singleton_ne_zero (h : ∀ a, μ {a} ≠ 0) :
    μ s = 0 ↔ s = ∅
Used by (1)

Actions: Source · Open Issue

Proof
by
  refine ⟨fun hs ↦ ?_, fun he ↦ by simp [he]⟩
  apply Set.eq_empty_of_forall_notMem
  exact fun a ha ↦ h a (measure_mono_null (Set.singleton_subset_iff.mpr ha) hs)
  1. MeasureTheory.measure_null_iff_eq_empty_of_measure_singleton_ne_zero