measurableSet_le — 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) \le g(a)\}$ является измеримым.$$

Lean4

theorem measurableSet_le (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_le_prod.measurableSet

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