instSFiniteOfNatMeasure

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

URI: https://scilib.ai/kg/mathlib#MeasureTheory.instSFiniteOfNatMeasure

English

The zero measure is s-finite: SFinite 0.

Русский

Нулевая мера является s-finite.

LaTeX

$$SFinite 0$$

Lean4

instance : SFinite (0 : Measure α) :=
  ⟨fun _ ↦ 0, inferInstance, by rw [Measure.sum_zero]⟩

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

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

Разделы

Аффилиация

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