measurable — Mathlib

English

A monotone function f from β to α, with β and α being suitable ordered measurable spaces, is measurable.

Русский

Непрерывно возрастающая функция f: β → α в подходящих упорядоченных измеримых пространствах измерима.

LaTeX

$$$\text{Monotone}(f) \Rightarrow \text{Measurable}(f)$$$

Lean4

protected theorem measurable [LinearOrder β] [OrderClosedTopology β] {f : β → α} (hf : Monotone f) : Measurable f :=
  suffices h : ∀ x, OrdConnected (f ⁻¹' Ioi x) from measurable_of_Ioi fun x => (h x).measurableSet
  fun _ => ordConnected_def.mpr fun _a ha _ _ _c hc => lt_of_lt_of_le ha (hf hc.1)

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