measure_eq_inducedOuterMeasure

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

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

English

μ s equals inducedOuterMeasure of the function f(s) = μ s.

Русский

μ s равно inducedOuterMeasure от функции f(s) = μ s.

LaTeX

$$$\mu s = \operatorname{inducedOuterMeasure}(f)(s) \quad\text{with } f(s)=\mu s$$$

Lean4

theorem measure_eq_inducedOuterMeasure : μ s = inducedOuterMeasure (fun s _ => μ s) MeasurableSet.empty μ.empty s :=
  measure_eq_trim _

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

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

Разделы

Аффилиация

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