measurable_to_countable — Mathlib

English

If α is countable and for every y ∈ β the fiber f^{-1}({f(y)}) is measurable, then f is measurable.

Русский

Если α счётно и для каждого y ∈ β множество f^{-1}({f(y)}) измеримо, то функция f измерима.

LaTeX

$$$\\forall y,\\ MeasurableSet(f^{-1} \\{f(y)\\}) \\implies Measurable f \\quad\\text{(with } α \\text{ countable)}$$$

Lean4

theorem measurable_to_countable [MeasurableSpace α] [Countable α] [MeasurableSpace β] {f : β → α}
    (h : ∀ y, MeasurableSet (f ⁻¹' {f y})) : Measurable f := fun s _ =>
  by
  rw [← biUnion_preimage_singleton]
  refine MeasurableSet.iUnion fun y => MeasurableSet.iUnion fun hy => ?_
  by_cases hyf : y ∈ range f
  · rcases hyf with ⟨y, rfl⟩
    apply h
  · simp only [preimage_singleton_eq_empty.2 hyf, MeasurableSet.empty]

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