ext_of_Ici — Mathlib

English

Let α be a Borel space with a linear order and finite measures μ, ν on α. If μ([a, ∞)) = ν([a, ∞)) for every a ∈ α, then μ = ν.

Русский

Пусть α — пространство Бореля с линейным порядком, μ и ν — конечные меры на α. Если для каждого a ∈ α выполняется μ([a, ∞)) = ν([a, ∞)), то μ = ν.

LaTeX

$$$\forall a, \mu([a, \infty)) = \nu([a, \infty)) \;\Rightarrow\; \mu = \nu$$$

Lean4

/-- Two finite measures on a Borel space are equal if they agree on all left-closed right-infinite
intervals. -/
theorem ext_of_Ici {α : Type*} [TopologicalSpace α] {_ : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α]
    [OrderTopology α] [BorelSpace α] (μ ν : Measure α) [IsFiniteMeasure μ] (h : ∀ a, μ (Ici a) = ν (Ici a)) : μ = ν :=
  @ext_of_Iic αᵒᵈ _ _ _ _ _ ‹_› _ _ _ h

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