measurable_of_Ioi — Mathlib

English

If a family of measurable functions has a pointwise least upper bound almost everywhere, then the bound function is measurable.

Русский

Если семейство измеримых функций имеет точечную наименьшую верхнюю границу почти повсюду, то граница измерима.

LaTeX

$$$\forall i, \text{Measurable}(f_i) \Rightarrow \text{IsLUB}(f_i) \Rightarrow \text{Measurable}(g)$$$

Lean4

theorem measurable_of_Ioi {f : δ → α} (hf : ∀ x, MeasurableSet (f ⁻¹' Ioi x)) : Measurable f :=
  by
  convert measurable_generateFrom (α := δ) _
  · exact BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ioi _)
  · rintro _ ⟨x, rfl⟩; exact hf x

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