ext_of_Ico_finite — Mathlib

English

Two finite measures μ and ν on a Borel space α are equal if they agree on all Ico(a,b) with a<b and μ(univ)=ν(univ).

Русский

Две конечные меры μ и ν на борелловом пространстве α равны, если они согласованы на всех Ico(a,b) при a<b и μ(α)=ν(α).

LaTeX

$$$(\mu = ν)$ given $(μ(\mathrm{Ico}(a,b)) = ν(\mathrm{Ico}(a,b)))$ for all a

Lean4

/-- Two finite measures on a Borel space are equal if they agree on all closed-open intervals. If `α` is a conditionally complete linear order with no top element, `MeasureTheory.Measure.ext_of_Ico` is an extensionality lemma with weaker assumptions on `μ` and `ν`. -/ theorem ext_of_Ico_finite {α : Type*} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ ν : Measure α) [IsFiniteMeasure μ] (hμν : μ univ = ν univ) (h : ∀ ⦃a b⦄, a < b → μ (Ico a b) = ν (Ico a b)) : μ = ν := by refine ext_of_generate_finite _ (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ico α)) (isPiSystem_Ico (id : α → α) id) ?_ hμν rintro - ⟨a, b, hlt, rfl⟩ exact h hlt

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