stronglyMeasurable_iff_measurable

English

The identity function id: α → α is strongly measurable when α has a suitable topology.

Русский

Функция тождества id: α → α является сильно измеримой при подходящей топологии пространства α.

LaTeX

$$$\text{StronglyMeasurable}(\mathrm{id})$$$

Lean4

/-- In a space with second countable topology, strongly measurable and measurable are equivalent. -/
theorem _root_.stronglyMeasurable_iff_measurable [TopologicalSpace β] [MetrizableSpace β] [BorelSpace β]
    [SecondCountableTopology β] : StronglyMeasurable f ↔ Measurable f :=
  ⟨fun h => h.measurable, fun h => Measurable.stronglyMeasurable h⟩

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