measureReal_restrict_apply'

Mathlib.MeasureTheory.Measure.Real

URI: https://scilib.ai/kg/mathlib#MeasureTheory.measureReal_restrict_apply'

← MathLib Explorer

English

For any measurable s, (μ|s).real t = μ.real (t ∩ s).

Русский

Для любого измеримого s, (μ|s).real t = μ.real(t ∩ s).

LaTeX

$$$ (\\mu \\restriction s).real t = \\mu.real (t \\cap s) $$$

Lean4

@[simp]
theorem measureReal_restrict_apply' (hs : MeasurableSet s) : (μ.restrict s).real t = μ.real (t ∩ s) := by
  simp only [measureReal_def, restrict_apply' hs]

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

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

Разделы

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

Аффилиация

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