English
A function f: α → ℕ∞ is measurable iff all its fibers over finite integers are measurable, i.e., f^{-1}({↑n}) is measurable for every n ∈ ℕ.
Русский
Функция f: α → ℕ∞ измерима тогда и только тогда, когда все её волокна над числами n ∈ ℕ измеримы, то есть f^{-1}({↑n}) измеримо для каждого n ∈ ℕ.
LaTeX
$$$\\text{Measurable}(f) \\iff \\forall n \\in \\mathbb{N},\\ MeasurableSet(f^{-1}(\\{\\uparrow n\\}))$$$
Lean4
theorem measurable_iff {α : Type*} [MeasurableSpace α] {f : α → ℕ∞} :
Measurable f ↔ ∀ n : ℕ, MeasurableSet (f ⁻¹' {↑n}) :=
by
refine ⟨fun hf n ↦ hf <| measurableSet_singleton _, fun h ↦ measurable_to_countable' fun n ↦ ?_⟩
cases n with
|
top =>
rw [← WithTop.none_eq_top, ← compl_range_some, preimage_compl, ← iUnion_singleton_eq_range, preimage_iUnion]
exact .compl <| .iUnion h
| coe n => exact h n
