measurable — Mathlib

English

If a function has measurable preimages of all intervals (x, ∞), then it is measurable.

Русский

Если прообраза каждого интервала (x, ∞) измерим, тогда функция измерима.

LaTeX

$$$\forall x,\ MeasurableSet(f^{-1}(Ioi(x))) \Rightarrow \ Measurable(f)$$$

Lean4

theorem measurable [TopologicalSpace δ] [OpensMeasurableSpace δ] {f : δ → α} (hf : UpperSemicontinuous f) :
    Measurable f :=
  measurable_of_Iio fun y => (hf.isOpen_preimage y).measurableSet

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