compl_toMeasurable_compl_ae_eq

Mathlib.MeasureTheory.Measure.NullMeasurable

URI: https://scilib.ai/kg/mathlib#MeasureTheory.NullMeasurableSet.compl_toMeasurable_compl_ae_eq

← MathLib Explorer

English

The complement under toMeasurable satisfies almost-everywhere equality with the complement of s.

Русский

Комплемент через toMeasurable совпадает почти наверно с комплементом s.

LaTeX

$$(toMeasurable μ s^c)^c =^μ s$$

Lean4

theorem compl_toMeasurable_compl_ae_eq (h : NullMeasurableSet s μ) : (toMeasurable μ sᶜ)ᶜ =ᵐ[μ] s :=
  Iff.mpr ae_eq_set_compl <| toMeasurable_ae_eq h.compl

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

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

Разделы

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

Аффилиация

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