measurable_mapNatBool — Mathlib

English

The map mapNatBool is a measurable function from α to the Cantor-like space ℕ → Bool.

Русский

Функция mapNatBool измерима как функция между соответствующими пространствами.

LaTeX

$$$\\text{measurable_mapNatBool} [MeasurableSpace α] [CountablyGenerated α] : Measurable (mapNatBool α)$$$

Lean4

theorem measurable_mapNatBool [MeasurableSpace α] [CountablyGenerated α] : Measurable (mapNatBool α) :=
  by
  rw [measurable_pi_iff]
  refine fun n ↦ measurable_to_bool ?_
  simp only [preimage, mem_singleton_iff, mapNatBool, Bool.decide_iff, setOf_mem_eq]
  apply measurableSet_natGeneratingSequence

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