le_trim

Mathlib.MeasureTheory.OuterMeasure.Induced

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

English

Trim is monotone with respect to outer measures: if m ≤ n, then m.trim ≤ n.trim.

Русский

Обрезка монотонна по отношению к внешним мерам: если m ≤ n, то m.trim ≤ n.trim.

LaTeX

$$$$ m \le n \quad \Longrightarrow \quad m^{\mathrm{trim}} \le n^{\mathrm{trim}}. $$$$

Lean4

theorem le_trim : m ≤ m.trim :=
  le_trim_iff.2 fun _ _ ↦ le_rfl

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

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

Разделы

Аффилиация

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