ext_of_Ioc' — Mathlib

English

Two measures μ,ν finite on α are equal if they agree on all Ioc(a,b) (open on left, closed on right).

Русский

Две конечные меры согласны по всем 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 α] [LinearOrder α]
    [OrderTopology α] [BorelSpace α] [NoMinOrder α] (μ ν : Measure α) (hμ : ∀ ⦃a b⦄, a < b → μ (Ioc a b) ≠ ∞)
    (h : ∀ ⦃a b⦄, a < b → μ (Ioc a b) = ν (Ioc a b)) : μ = ν :=
  by
  refine @ext_of_Ico' αᵒᵈ _ _ _ _ _ ‹_› _ μ ν ?_ ?_ <;> intro a b hab <;> erw [Ico_toDual (α := α)]
  exacts [hμ hab, h hab]

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