boundedBy_top

Mathlib.MeasureTheory.OuterMeasure.OfFunction

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

← MathLib Explorer

English

The boundedBy construction is compatible with the top outer measure: boundedBy(⊤) = ⊤.

Русский

Пусть ⊤ — наивысшая внешняя мера; тогда boundedBy(⊤) = ⊤.

LaTeX

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

Lean4

@[simp]
theorem boundedBy_top : boundedBy (⊤ : Set α → ℝ≥0∞) = ⊤ :=
  by
  rw [eq_top_iff, le_boundedBy']
  intro s hs
  rw [top_apply hs]
  exact le_rfl

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

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

Разделы

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

Аффилиация

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