measurable_of_Ici — Mathlib

English

If all sets {f^{-1}(Ici x)} are measurable, then f is measurable.

Русский

Если для всех x множество f^{-1}(Ici x) измеримо, тогда функция измерима.

LaTeX

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

Lean4

theorem measurable_of_Ici {f : δ → α} (hf : ∀ x, MeasurableSet (f ⁻¹' Ici x)) : Measurable f :=
  by
  apply measurable_of_Iio
  simp_rw [← compl_Ici, preimage_compl, MeasurableSet.compl_iff]
  assumption

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