English
For countable α, μ1 = μ2 if and only if μ1.real({x}) = μ2.real({x}) for all x, provided both measures are sigma-finite.
Русский
Для счётного α, μ1 = μ2 тогда и только тогда, когда μ1.real({x}) = μ2.real({x}) для всех x, при условии, что μ1 и μ2 — сигма-конечны.
LaTeX
$$$ [Countable α] [SigmaFinite μ1] [SigmaFinite μ2] : μ1 = μ2 \\iff ∀ x, μ1.real { x } = μ2.real { x } $$$
Lean4
theorem _root_.MeasureTheory.ext_iff_measureReal_singleton [Countable α] {μ1 μ2 : Measure α} [SigmaFinite μ1]
[SigmaFinite μ2] : μ1 = μ2 ↔ ∀ x, μ1.real { x } = μ2.real { x } :=
by
rw [Measure.ext_iff_singleton]
congr! with x
rw [measureReal_def, measureReal_def, ENNReal.toReal_eq_toReal_iff]
simp [measure_singleton_lt_top, ne_of_lt]