trim_trim

Mathlib.MeasureTheory.OuterMeasure.Induced

URI: https://scilib.ai/kg/mathlib#MeasureTheory.OuterMeasure.trim_trim

English

Applying trim twice yields the same result: m.trim.trim = m.trim.

Русский

Повторное применение обрезки даёт тот же результат: m.trim.trim = m.trim.

LaTeX

$$$$ m^{\mathrm{trim}}_{\mathrm{trim}} = m^{\mathrm{trim}}. $$$$

Lean4

theorem trim_trim (m : OuterMeasure α) : m.trim.trim = m.trim :=
  trim_eq_trim_iff.2 fun _s => m.trim_eq

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

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

Разделы

Аффилиация

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