measurable_inclusion

Mathlib.MeasureTheory.MeasurableSpace.Constructions

URI: https://scilib.ai/kg/mathlib#measurable_inclusion

English

If s ⊆ t, the inclusion map s → t is measurable.

Русский

Если s ⊆ t, то включение s → t измеримо.

LaTeX

$$$\\\\operatorname{Measurable}(\\\\text{inclusion}(h))$$$

Lean4

theorem measurable_inclusion {s t : Set α} (h : s ⊆ t) : Measurable (inclusion h) :=
  measurable_id.subtype_map h

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

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

Разделы

Аффилиация

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