innerContent_mono'

Mathlib.MeasureTheory.Measure.Content

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

← MathLib Explorer

English

For an open U, μ.outerMeasure U = μ.innerContent U.

Русский

Для открытого U: μ.outerMeasure U = μ.innerContent U.

LaTeX

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

Lean4

theorem innerContent_mono' ⦃U V : Set G⦄ (hU : IsOpen U) (hV : IsOpen V) (h2 : U ⊆ V) :
    μ.innerContent ⟨U, hU⟩ ≤ μ.innerContent ⟨V, hV⟩ :=
  biSup_mono fun _ hK => hK.trans h2

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

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

Разделы

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

Аффилиация

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