_example

Mathlib.MeasureTheory.Measure.Haar.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure._example

← MathLib Explorer

English

Second-countable implies sigma-finiteness of Haar measure.

Русский

Вторая счётность приводит к сигма-конечности меры Хаара.

LaTeX

$$SigmaFinite (haarMeasure K0)$$

Lean4

example [LocallyCompactSpace G] (μ : Measure G) [IsHaarMeasure μ] (K₀ : PositiveCompacts G) :
    μ = μ K₀.1 • haarMeasure K₀ :=
  haarMeasure_unique μ K₀

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

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

Разделы

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

Аффилиация

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