lt_top

Mathlib.MeasureTheory.Measure.Content

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

English

For every compact K, μ(K) < ∞.

Русский

Для каждого компактного K выполняется μ(K) < ∞.

LaTeX

$$$\mu(K) < \infty$$$

Lean4

theorem lt_top (K : Compacts G) : μ K < ∞ :=
  ENNReal.coe_lt_top

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

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

Разделы

Аффилиация

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