Lean4
/-- Two measures which are finite on closed-open intervals are equal if they agree on all
closed-open intervals. -/
theorem ext_of_Ico' {α : Type*} [TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α] [LinearOrder α]
[OrderTopology α] [BorelSpace α] [NoMaxOrder α] (μ ν : Measure α) (hμ : ∀ ⦃a b⦄, a < b → μ (Ico a b) ≠ ∞)
(h : ∀ ⦃a b⦄, a < b → μ (Ico a b) = ν (Ico a b)) : μ = ν :=
by
rcases exists_countable_dense_bot_top α with ⟨s, hsc, hsd, hsb, _⟩
have : (⋃ (l ∈ s) (u ∈ s) (_ : l < u), {Ico l u} : Set (Set α)).Countable :=
hsc.biUnion fun l _ => hsc.biUnion fun u _ => countable_iUnion fun _ => countable_singleton _
simp only [← setOf_eq_eq_singleton, ← setOf_exists] at this
refine
Measure.ext_of_generateFrom_of_cover_subset (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ico α))
(isPiSystem_Ico id id) ?_ this ?_ ?_ ?_
· rintro _ ⟨l, -, u, -, h, rfl⟩
exact ⟨l, u, h, rfl⟩
· refine sUnion_eq_univ_iff.2 fun x => ?_
rcases hsd.exists_le' hsb x with ⟨l, hls, hlx⟩
rcases hsd.exists_gt x with ⟨u, hus, hxu⟩
exact ⟨_, ⟨l, hls, u, hus, hlx.trans_lt hxu, rfl⟩, hlx, hxu⟩
· rintro _ ⟨l, -, u, -, hlt, rfl⟩
exact hμ hlt
· rintro _ ⟨l, u, hlt, rfl⟩
exact h hlt
