withDensity_indicator_one

Mathlib.MeasureTheory.Measure.WithDensity

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

← MathLib Explorer

English

If s is measurable, then μ.withDensity(s.indicator 1) equals μ.restrict s.

Русский

Если s измеримо, то μ.withDensity(s.indicator 1) равняется μ.restrict s.

LaTeX

$$$\\mu.withDensity(s.indicator 1) = \\mu.restrict s$$$

Lean4

theorem withDensity_indicator_one {s : Set α} (hs : MeasurableSet s) : μ.withDensity (s.indicator 1) = μ.restrict s :=
  by rw [withDensity_indicator hs, withDensity_one]

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

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

Разделы

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

Аффилиация

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