toMeasure_apply

Mathlib.MeasureTheory.Measure.MeasureSpace

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

← MathLib Explorer

English

For all measurable h and measurable s, the equality m.toMeasure h s = m s holds.

Русский

Для всех измеримых h и измеримых s выполняется m.toMeasure h s = m s.

LaTeX

$$$$ m.toMeasure(h)(s) = m(s) \quad\text{for measurable } s.$$$$

Lean4

@[simp]
theorem toMeasure_apply (m : OuterMeasure α) (h : ms ≤ m.caratheodory) {s : Set α} (hs : MeasurableSet s) :
    m.toMeasure h s = m s :=
  m.trim_eq hs

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

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

Разделы

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

Аффилиация

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