nullMeasurableSet

Mathlib.MeasureTheory.Measure.NullMeasurable

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

← MathLib Explorer

English

If f is a measurable embedding and μ ⟂ₘ ν, then μ.map f ⟂ₘ ν.map f.

Русский

Если f - измеримо вложение и μ ⟂ₘ ν, то μ.map f ⟂ₘ ν.map f.

LaTeX

$$$$ \\mu.map f \\perp_{m} \\nu.map f. $$$$

Lean4

@[simp, aesop unsafe (rule_sets := [Measurable])]
theorem _root_.MeasurableSet.nullMeasurableSet (h : MeasurableSet s) : NullMeasurableSet s μ :=
  h.eventuallyMeasurableSet

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

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

Разделы

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

Аффилиация

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