measurableSet_lt — Mathlib

English

The set {a | f(a) < g(a)} is measurable when f,g are strongly measurable.

Русский

Множество {a | f(a) < g(a)} измеримо, если f,g — сильно измеримы.

LaTeX

$$$\{a \mid f(a) < g(a)\}$ измеримо; при этом $f,g$ сильно измеримы.$$

Lean4

theorem measurableSet_lt (hf : StronglyMeasurable[m] f) (hg : StronglyMeasurable[m] g) :
    MeasurableSet[m] {a | f a < g a} := by
  simpa only [lt_iff_le_not_ge] using (hf.measurableSet_le hg).inter (hg.measurableSet_le hf).compl

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