English
If f,g: α → E are measurable into a group E (or ordered group) with appropriate measurability assumptions, then the set {x ∈ α : f(x) = g(x)} is measurable.
Русский
Пусть f,g: α → E измеримы в группе E; множество {x ∈ α | f(x)=g(x)} измеримо.
LaTeX
$$$\\{x\\in α\\mid f(x)=g(x)\\}$ является измеримым множеством$$
Lean4
@[measurability]
theorem measurableSet_eq_fun {m : MeasurableSpace α} {E} [MeasurableSpace E] [AddGroup E] [MeasurableSingletonClass E]
[MeasurableSub₂ E] {f g : α → E} (hf : Measurable f) (hg : Measurable g) : MeasurableSet {x | f x = g x} :=
by
suffices h_set_eq : {x : α | f x = g x} = {x | (f - g) x = (0 : E)}
by
rw [h_set_eq]
exact (hf.sub hg) measurableSet_eq
ext
simp_rw [Set.mem_setOf_eq, Pi.sub_apply, sub_eq_zero]
