image_inclusion

Mathlib.MeasureTheory.MeasurableSpace.Constructions

URI: https://scilib.ai/kg/mathlib#MeasurableSet.image_inclusion

← MathLib Explorer

English

If s ⊆ t and s, u are measurable, then the image inclusion is measurable.

Русский

Если s ⊆ t и s, u измеримы, то образующее включение измеримо.

LaTeX

$$$\\\\operatorname{image\\\\_inclusion}(h)$$$$

Lean4

theorem image_inclusion {s t : Set α} (h : s ⊆ t) {u : Set s} (hs : MeasurableSet s) (hu : MeasurableSet u) :
    MeasurableSet (inclusion h '' u) :=
  (measurable_subtype_coe hs).image_inclusion' h hu

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

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

Разделы

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

Аффилиация

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