English
Variant formulation ensuring two distinct target neighborhoods with positive preimage measure under μ.
Русский
Вариант формулировки, гарантирующий две различные окрестности с положительной мерой прообраза.
LaTeX
$$$\exists a,b\ (a\neq b) \wedge (∀ s∈\mathcal{N}(a), μ(f^{-1}(s))>0) ∧ (∀ t∈\mathcal{N}(b), μ(f^{-1}(t))>0)$$$
Lean4
/-- If two finite measures give the same mass to the whole space and coincide on a π-system made
of measurable sets, then they coincide on all sets in the σ-algebra generated by the π-system. -/
theorem ext_on_measurableSpace_of_generate_finite {α} (m₀ : MeasurableSpace α) {μ ν : Measure α} [IsFiniteMeasure μ]
(C : Set (Set α)) (hμν : ∀ s ∈ C, μ s = ν s) {m : MeasurableSpace α} (h : m ≤ m₀)
(hA : m = MeasurableSpace.generateFrom C) (hC : IsPiSystem C) (h_univ : μ Set.univ = ν Set.univ) {s : Set α}
(hs : MeasurableSet[m] s) : μ s = ν s :=
by
haveI : IsFiniteMeasure ν := by
constructor
rw [← h_univ]
apply IsFiniteMeasure.measure_univ_lt_top
induction s, hs using induction_on_inter hA hC with
| empty => simp
| basic t ht => exact hμν t ht
| compl t htm iht =>
rw [measure_compl (h t htm) (measure_ne_top _ _), measure_compl (h t htm) (measure_ne_top _ _), iht, h_univ]
| iUnion f hfd hfm ihf => simp [measure_iUnion, hfd, h _ (hfm _), ihf]
