English
Under standard assumptions for additive groups with measurable Sub₂, the set {x | f(x) = g(x)} is measurable whenever f,g are measurable.
Русский
При стандартных предположениях для аддитивных групп с measurable Sub₂ множество {x | f(x)=g(x)} измеримо при измеримых f,g.
LaTeX
$$$\\{x\\in α\\mid f(x)=g(x)\\}$ измеримо$$
Lean4
@[measurability]
theorem measurableSet_eq_fun' {β : Type*} [AddCommMonoid β] [PartialOrder β] [CanonicallyOrderedAdd β] [Sub β]
[OrderedSub β] {_ : MeasurableSpace β} [MeasurableSub₂ β] [MeasurableSingletonClass β] {f g : α → β}
(hf : Measurable f) (hg : Measurable g) : MeasurableSet {x | f x = g x} :=
by
have : {a | f a = g a} = {a | (f - g) a = 0} ∩ {a | (g - f) a = 0} :=
by
ext
simp only [Set.mem_setOf_eq, Pi.sub_apply, tsub_eq_zero_iff_le, Set.mem_inter_iff]
exact ⟨fun h ↦ ⟨h.le, h.symm.le⟩, fun h ↦ le_antisymm h.1 h.2⟩
rw [this]
exact ((hf.sub hg) (measurableSet_singleton 0)).inter ((hg.sub hf) (measurableSet_singleton 0))
