trimmed

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.trimmed

English

For any μ, the trimmed outer measure equals the outer measure: μ.toOuterMeasure.trim = μ.toOuterMeasure.

Русский

Для любой μ выполняется равенство: μ.toOuterMeasure.trim = μ.toOuterMeasure.

LaTeX

$$$ (\mu.toOuterMeasure).trim = \mu.toOuterMeasure $$$

Lean4

theorem trimmed (μ : Measure α) : μ.toOuterMeasure.trim = μ.toOuterMeasure :=
  le_antisymm μ.trim_le μ.1.le_trim

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

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

Разделы

Аффилиация

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