measurable — Mathlib

English

If f is a closed embedding between topological spaces, then f is a measurable function (with respect to the Borel σ-algebras).

Русский

Пусть f является замкнутым вложением между топологическими пространствами; тогда f измерима по соответствующим борелевским σ‑алгебрам.

LaTeX

$$$\\forall f:\\alpha\\to\\beta\\,,\\ IsClosedEmbedding(f)\\Rightarrow\\mathrm{Measurable}(f)$$$

Lean4

theorem measurable {f : α → γ} (hf : IsClosedEmbedding f) : Measurable f :=
  hf.continuous.measurable

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