exists_measurable_superset_of_null

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

URI: https://scilib.ai/kg/mathlib#MeasureTheory.exists_measurable_superset_of_null

English

If μ s = 0, then there exists t ⊇ s with t measurable and μ t = 0.

Русский

Если μ s = 0, существует измеримое надмножество t ⊇ s с μ t = 0.

LaTeX

$$$\exists t, s \subseteq t \wedge MeasurableSet t \wedge μ t = 0$$$

Lean4

theorem exists_measurable_superset_of_null (h : μ s = 0) : ∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = 0 :=
  h ▸ exists_measurable_superset μ s

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

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

Разделы

Аффилиация

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