outerMeasure_opens

Mathlib.MeasureTheory.Measure.Content

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

← MathLib Explorer

English

For open U, outer measure equals inner content.

Русский

Для открытого U внешняя мера равна внутренному содержимому.

LaTeX

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

Lean4

theorem outerMeasure_opens (U : Opens G) : μ.outerMeasure U = μ.innerContent U :=
  inducedOuterMeasure_eq' (fun _ => isOpen_iUnion) μ.innerContent_iUnion_nat μ.innerContent_mono U.2

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

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

Разделы

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

Аффилиация

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