instSigmaFiniteElemRealIoiOfNatVolumeIoiPow

Mathlib.MeasureTheory.Constructions.HaarToSphere

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

English

For every natural number n, the measure volumeIoiPow(n) on the real line is sigma-finite.

Русский

Для каждого натурального числа n мера volumeIoiPow(n) на вещественной оси сигма-ограничена.

LaTeX

$$\forall n, \text{SigmaFinite}(\mathrm{volumeIoiPow}(n))$$

Lean4

instance (n : ℕ) : SigmaFinite (volumeIoiPow n) :=
  (finiteSpanningSetsIn_volumeIoiPow_range_Iio n).sigmaFinite

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

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

Разделы

Аффилиация

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