measurable_to_bool — Mathlib

English

If the preimage of {true} under f: α → Bool is measurable, then f is measurable.

Русский

Если f^{-1}({true}) измеримо, то f измерима.

LaTeX

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

Lean4

theorem measurable_to_bool {f : α → Bool} (h : MeasurableSet (f ⁻¹' { true })) : Measurable f :=
  by
  apply measurable_to_countable'
  rintro (- | -)
  · convert h.compl
    rw [← preimage_compl, Bool.compl_singleton, Bool.not_true]
  exact h

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