null_of_trim_null

Mathlib.MeasureTheory.OuterMeasure.Induced

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

English

If the trim of a set is zero, then the outer measure of the set is zero.

Русский

Если обрезка множества равна нулю, то внешняя мера множества равна нулю.

LaTeX

$$$$ m^{\mathrm{trim}}(s) = 0 \Rightarrow m(s) = 0. $$$$

Lean4

theorem null_of_trim_null {s : Set α} (h : m.trim s = 0) : m s = 0 :=
  nonpos_iff_eq_zero.1 <| (le_trim m s).trans_eq h

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

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

Разделы

Аффилиация

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