English
If α is MeasurableSingletonClass and f agrees with a measurable g except on a countable set, then f is measurable.
Русский
Если f совпадает с измеримой g за исключением счётного множества, тогда f измерима.
LaTeX
$$$\\text{MeasurableSingletonClass } \\alpha \\Rightarrow \\text{Measurable } f \\to \\ (\\{x \\mid f(x) \\neq g(x)\\}\\text{Countable}) \\Rightarrow \\text{Measurable } g$$$
Lean4
/-- If a function coincides with a measurable function outside of a countable set, it is
measurable. -/
theorem measurable_of_countable_ne [MeasurableSingletonClass α] (hf : Measurable f)
(h : Set.Countable {x | f x ≠ g x}) : Measurable g :=
by
intro t ht
have : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x} := by simp [← inter_union_distrib_left]
rw [this]
refine (h.mono inter_subset_right).measurableSet.union ?_
have : g ⁻¹' t ∩ {x : α | f x = g x} = f ⁻¹' t ∩ {x : α | f x = g x} :=
by
ext x
simp +contextual
rw [this]
exact (hf ht).inter h.measurableSet.of_compl
