zero_trim

Mathlib.MeasureTheory.Measure.Trim

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

English

The trim of the zero measure is zero: (0: Measure α).trim hm = 0 for any hm.

Русский

Обрезка нулевой меры даёт нуль: (0: Measure α).trim hm = 0.

LaTeX

$$$0^{\\mathrm{trim}(hm)} = 0.$$$

Lean4

@[simp]
theorem zero_trim (hm : m ≤ m0) : (0 : Measure α).trim hm = (0 : @Measure α m) := by
  simp [Measure.trim, @OuterMeasure.toMeasure_zero _ m]

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

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

Разделы

Аффилиация

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