measurable_of_Iic — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem measurable_of_Iic {f : δ → α} (hf : ∀ x, MeasurableSet (f ⁻¹' Iic x)) : Measurable f :=
  by
  apply measurable_of_Ioi
  simp_rw [← compl_Iic, preimage_compl, MeasurableSet.compl_iff]
  assumption

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