empty

Mathlib.MeasureTheory.Measure.Content

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

English

The content of the empty compact is zero: μ(⊥) = 0.

Русский

Контент пустого компактного множества равен нулю: μ(⊥) = 0.

LaTeX

$$$\mu(\perp) = 0$$$

Lean4

theorem empty : μ ⊥ = 0 := by simpa [toNNReal_eq_zero_iff] using μ.sup_disjoint' ⊥ ⊥

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

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

Разделы

Аффилиация

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