measurableSet_lt — Mathlib

English

If f,g: δ → α are measurable, then the set {a ∈ δ | f(a) < g(a)} is measurable.

Русский

Для измеримых отображений f,g: δ → α множество {a∈δ | f(a) < g(a)} измеримо.

LaTeX

$$$\text{MeasurableSet}\{a\in\delta \mid f(a) < g(a)\}$$$

Lean4

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

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