outerMeasure

Mathlib.MeasureTheory.Measure.Content

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Content.outerMeasure

← MathLib Explorer

English

For any open U, μ.outerMeasure U equals μ.innerContent U.

Русский

Для любого открытого U, μ.outerMeasure U эквивалентно μ.innerContent U.

LaTeX

$$$\mu.outerMeasure(U) = \mu.innerContent(U)$ for open U.$$

Lean4

/-- Extending a content on compact sets to an outer measure on all sets. -/
protected def outerMeasure : OuterMeasure G :=
  inducedOuterMeasure (fun U hU => μ.innerContent ⟨U, hU⟩) isOpen_empty μ.innerContent_bot

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

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

Разделы

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

Аффилиация

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