measurableSet_range

Mathlib.MeasureTheory.MeasurableSpace.Embedding

URI: https://scilib.ai/kg/mathlib#MeasurableEmbedding.measurableSet_range

← MathLib Explorer

English

If f is a MeasurableEmbedding, then range f is measurable.

Русский

Если f — измеримое вложение, то образ диапазона f измерим.

LaTeX

$$$\\text{MeasurableEmbedding}(f) \\Rightarrow \\text{MeasurableSet}(\\text{range}(f)).$$$

Lean4

theorem measurableSet_range (hf : MeasurableEmbedding f) : MeasurableSet (range f) :=
  by
  rw [← image_univ]
  exact hf.measurableSet_image' MeasurableSet.univ

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru