borel_measurable — Mathlib

English

If f: α → β is continuous, then f is measurable with respect to the Borel sigma-algebras on α and β.

Русский

Если f: α → β непрерывна, то она измерима относительно борелевых сигма-алгебр на α и β.

LaTeX

$$$$ \text{Continuous } f \Rightarrow \text{Measurable}(f) \text{ w.r.t. } \mathrm{borel}(\alpha) \text{ and } \mathrm{borel}(\beta). $$$$

Lean4

theorem borel_measurable [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) :
    @Measurable α β (borel α) (borel β) f :=
  Measurable.of_le_map <| generateFrom_le fun s hs => GenerateMeasurable.basic (f ⁻¹' s) (hs.preimage hf)

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