measurableSet_eq_fun — Mathlib

English

If f and g are strongly measurable, then the set where f equals g is a measurable set.

Русский

Если f и g сильно измеримы, то множество точек, где f(x)=g(x), измеримо.

LaTeX

$$$\{ x \in \alpha : f(x)=g(x) \} \in m$$$

Lean4

theorem measurableSet_eq_fun (hf : StronglyMeasurable[m] f) (hg : StronglyMeasurable[m] g) :
    MeasurableSet[m] {a | f a = g a} := by
  borelize (E × E)
  exact (hf.prodMk hg).measurable isClosed_diagonal.measurableSet

Похожие утверждения