boundedBy_eq_self

Mathlib.MeasureTheory.OuterMeasure.OfFunction

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

← MathLib Explorer

English

For any outer measure m, boundedBy m equals m itself.

Русский

Для любой внешней меры m справедливо, что boundedBy m = m.

LaTeX

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

Lean4

@[simp]
theorem boundedBy_eq_self (m : OuterMeasure α) : boundedBy m = m :=
  ext fun _ => boundedBy_eq _ measure_empty (fun _ ht => measure_mono ht) measure_iUnion_le

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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