English
If E is countable and f,g: α → E are measurable, then the equality set {x | f(x) = g(x)} is measurable.
Русский
Если кодом E является счётное множество и f,g: α → E измеримы, то множество равенств {x | f(x)=g(x)} измеримо.
LaTeX
$$$\\text{MeasurableSet}\\{x\\mid f(x)=g(x)\\}$$$
Lean4
theorem measurableSet_eq_fun_of_countable {m : MeasurableSpace α} {E} [MeasurableSpace E] [MeasurableSingletonClass E]
[Countable E] {f g : α → E} (hf : Measurable f) (hg : Measurable g) : MeasurableSet {x | f x = g x} :=
by
have : {x | f x = g x} = ⋃ j, {x | f x = j} ∩ {x | g x = j} :=
by
ext1 x
simp only [Set.mem_setOf_eq, Set.mem_iUnion, Set.mem_inter_iff, exists_eq_right']
rw [this]
refine MeasurableSet.iUnion fun j => MeasurableSet.inter ?_ ?_
· exact hf (measurableSet_singleton j)
· exact hg (measurableSet_singleton j)
