English
Dirac measures at x and y are equal if and only if x equals y.
Русский
Меры Дирака δ_x и δ_y равны тогда и только тогда, когда x = y.
LaTeX
$$$\\mathrm{dirac}_x = \\mathrm{dirac}_y \\iff x = y$$$
Lean4
/-- Dirac delta measures at two points are equal if every measurable set contains either both or
neither of the points. -/
theorem dirac_eq_dirac_iff_forall_mem_iff_mem {x y : α} :
Measure.dirac x = Measure.dirac y ↔ ∀ A, MeasurableSet A → (x ∈ A ↔ y ∈ A) :=
by
constructor
· intro h A A_mble
have obs := congr_arg (fun μ ↦ μ A) h
simp only [Measure.dirac_apply' _ A_mble] at obs
by_cases x_in_A : x ∈ A
·
simpa only [x_in_A, indicator_of_mem, Pi.one_apply, true_iff, Eq.comm (a := (1 : ℝ≥0∞)),
indicator_eq_one_iff_mem] using obs
·
simpa only [x_in_A, indicator_of_notMem, Eq.comm (a := (0 : ℝ≥0∞)), indicator_apply_eq_zero, false_iff,
not_false_eq_true, Pi.one_apply, one_ne_zero, imp_false] using obs
· intro h
ext A A_mble
by_cases x_in_A : x ∈ A
· simp only [Measure.dirac_apply' _ A_mble, x_in_A, indicator_of_mem, Pi.one_apply, (h A A_mble).mp x_in_A]
· have y_notin_A : y ∉ A := by simp_all only [not_false_eq_true]
simp only [Measure.dirac_apply' _ A_mble, x_in_A, y_notin_A, not_false_eq_true, indicator_of_notMem]
