trim_add

Mathlib.MeasureTheory.Measure.Trim

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

← MathLib Explorer

English

The trim operation is additive over measures: (μ + ν).trim hm = μ.trim hm + ν.trim hm.

Русский

Обрезка меры аддитивна по сумме мер: (μ + ν).trim hm = μ.trim hm + ν.trim hm.

LaTeX

$$$(μ + ν).trim hm = μ.trim hm + ν.trim hm.$$$

Lean4

theorem trim_add {ν : Measure α} (hm : m ≤ m0) : (μ + ν).trim hm = μ.trim hm + ν.trim hm :=
  @Measure.ext _ m _ _ (fun s hs ↦ by simp [trim_measurableSet_eq hm hs])

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

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

Разделы

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

Аффилиация

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