English
Dirac measures at x and y are different if there exists a measurable set that contains one of the points but not the other.
Русский
Меры Дирака δ_x и δ_y различны, если существует измеримое множество, содержащее одну точку, но не другую.
LaTeX
$$$\\mathrm{dirac}_x \\neq \\mathrm{dirac}_y \\iff \\exists A, \\text{MeasurableSet}(A) \\land x \\in A \\land y \\notin A$$$
Lean4
/-- Dirac delta measures at two points are different if and only if there is a measurable set
containing one of the points but not the other. -/
theorem dirac_ne_dirac_iff_exists_measurableSet {x y : α} :
Measure.dirac x ≠ Measure.dirac y ↔ ∃ A, MeasurableSet A ∧ x ∈ A ∧ y ∉ A :=
by
apply not_iff_not.mp
simp only [ne_eq, not_not, not_exists, not_and, dirac_eq_dirac_iff_forall_mem_iff_mem]
refine ⟨fun h A A_mble ↦ by simp only [h A A_mble, imp_self], fun h A A_mble ↦ ?_⟩
by_cases x_in_A : x ∈ A
· simp only [x_in_A, h A A_mble x_in_A]
· simpa only [x_in_A, false_iff] using h Aᶜ (MeasurableSet.compl_iff.mpr A_mble) x_in_A
