boundedBy_zero

Mathlib.MeasureTheory.OuterMeasure.OfFunction

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

English

Zero boundedBy is the zero outer measure: boundedBy(0) = 0.

Русский

Нулевая boundedBy равна нулевой внешней мере: boundedBy(0) = 0.

LaTeX

$$$\\mathrm{boundedBy}(0) = 0$$$

Lean4

@[simp]
theorem boundedBy_zero : boundedBy (0 : Set α → ℝ≥0∞) = 0 :=
  by
  rw [← coe_bot, eq_bot_iff]
  apply boundedBy_le

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

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

Разделы

Аффилиация

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