ext_of_Ioc — Mathlib

English

Two finite measures μ and ν on α are equal if they agree on all open‑closed intervals Ioc a b.

Русский

Две конечные меры равны, если они согласны на всех открыто‑закрытых интервалах Ioc a b.

LaTeX

$$$\forall a

Lean4

/-- Two measures which are finite on closed-open intervals are equal if they agree on all
open-closed intervals. -/
theorem ext_of_Ioc {α : Type*} [TopologicalSpace α] {_m : MeasurableSpace α} [SecondCountableTopology α]
    [ConditionallyCompleteLinearOrder α] [OrderTopology α] [BorelSpace α] [NoMinOrder α] (μ ν : Measure α)
    [IsLocallyFiniteMeasure μ] (h : ∀ ⦃a b⦄, a < b → μ (Ioc a b) = ν (Ioc a b)) : μ = ν :=
  μ.ext_of_Ioc' ν (fun _ _ _ => measure_Ioc_lt_top.ne) h

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