measurableSet_le — Mathlib

English

If f,g are measurable functions from δ to α, then {a ∈ δ | f(a) ≤ g(a)} is measurable.

Русский

Если f,g — измеримые отображения δ → α, то множество {a ∈ δ | f(a) ≤ g(a)} измеримо.

LaTeX

$$$\{a \in \delta \mid f(a) \le g(a)\} \in \mathcal{M}_{\delta}$.$$

Lean4

@[measurability]
theorem measurableSet_le {f g : δ → α} (hf : Measurable f) (hg : Measurable g) : MeasurableSet {a | f a ≤ g a} :=
  hf.prodMk hg measurableSet_le'

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