measure_ext_Ioo_rat — Mathlib

English

If two locally finite measures μ,ν on R agree on all open intervals Ioo with rational endpoints, then μ = ν.

Русский

Если две locally-finite меры μ, ν на ℝ согласованы на все открытые интервалы Ioo с рациональными границами, то μ = ν.

LaTeX

$$$\\\\forall μ ν : \\\\mathrm{Measure}(\\\\mathbb{R}), [\\\\operatorname{IsLocallyFiniteMeasure} μ], [\\\\operatorname{IsLocallyFiniteMeasure} ν], (\\\\forall a,b \\\\in \\\\mathbb{Q}, μ(Ioo(a,b)) = ν(Ioo(a,b))) \\\\Rightarrow μ = ν$$$

Lean4

theorem measure_ext_Ioo_rat {μ ν : Measure ℝ} [IsLocallyFiniteMeasure μ] (h : ∀ a b : ℚ, μ (Ioo a b) = ν (Ioo a b)) :
    μ = ν :=
  (finiteSpanningSetsInIooRat μ).ext borel_eq_generateFrom_Ioo_rat isPiSystem_Ioo_rat <|
    by
    simp only [mem_iUnion, mem_singleton_iff]
    rintro _ ⟨a, b, -, rfl⟩
    apply h

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