measure_interior_of_null_frontier

Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

URI: https://scilib.ai/kg/mathlib#measure_interior_of_null_frontier

← MathLib Explorer

English

If μ(frontier s) = 0, then μ(interior s) = μ(s).

Русский

Если μ( frontier s ) = 0, тогда μ( interior s ) = μ(s).

LaTeX

$$$\\mu(\\operatorname{frontier}(s)) = 0 \\Rightarrow \\mu(\\operatorname{interior}(s)) = \\mu(s).$$$

Lean4

theorem measure_interior_of_null_frontier {μ : Measure α'} {s : Set α'} (h : μ (frontier s) = 0) :
    μ (interior s) = μ s :=
  measure_congr (interior_ae_eq_of_null_frontier h)

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

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

Разделы

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

Аффилиация

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