measurable_to_prop — Mathlib

English

If f: α → Prop has measurable preimage of True, then f is measurable.

Русский

Если f: α → Prop имеет измеримое предобраз True, то f измерима.

LaTeX

$$$\\MeasurableSet( f^{-1}(\\{ \\text{True} \\} )) \\Rightarrow Measurable f$$$

Lean4

theorem measurable_to_prop {f : α → Prop} (h : MeasurableSet (f ⁻¹' { True })) : Measurable f :=
  by
  refine measurable_to_countable' fun x => ?_
  by_cases hx : x
  · simpa [hx] using h
  · simpa only [hx, ← preimage_compl, «Prop».compl_singleton, not_true, preimage_singleton_false] using h.compl

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