ext_iff_measureReal_singleton — Mathlib

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]

Похожие утверждения