measure_eq_extend

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

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

English

For any s with measurability, μ s equals extend of the function t ↦ μ t on s.

Русский

Для измеримого s, μ s равно extend (t ↦ μ t) на s.

LaTeX

$$$\mu s = \operatorname{extend}(\lambda t\;\_\;\Rightarrow \mu t)\ s$$$

Lean4

theorem measure_eq_extend (hs : MeasurableSet s) : μ s = extend (fun t (_ht : MeasurableSet t) => μ t) s :=
  by
  rw [extend_eq]
  exact hs

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

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

Разделы

Аффилиация

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