English
If μ(Iic a) = ν(Iic a) for all a, then μ = ν.
Русский
Если μ(Iic a)=ν(Iic a) для всех a, тогда μ=ν.
LaTeX
$$$(\forall a, μ(Iic(a)) = ν(Iic(a))) \Rightarrow μ=ν$$$
Lean4
/-- Two finite measures on a Borel space are equal if they agree on all left-infinite right-closed
intervals. -/
theorem ext_of_Iic {α : Type*} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α]
[OrderTopology α] [BorelSpace α] (μ ν : Measure α) [IsFiniteMeasure μ] (h : ∀ a, μ (Iic a) = ν (Iic a)) : μ = ν :=
by
refine ext_of_Ioc_finite μ ν ?_ fun a b hlt => ?_
· rcases exists_countable_dense_bot_top α with ⟨s, hsc, hsd, -, hst⟩
have : DirectedOn (· ≤ ·) s := directedOn_iff_directed.2 (Subtype.mono_coe _).directed_le
simp only [← biSup_measure_Iic hsc (hsd.exists_ge' hst) this, h]
rw [← Iic_diff_Iic, measure_diff (Iic_subset_Iic.2 hlt.le) nullMeasurableSet_Iic,
measure_diff (Iic_subset_Iic.2 hlt.le) nullMeasurableSet_Iic, h a, h b]
· rw [← h a]
exact measure_ne_top μ _
· exact measure_ne_top μ _
