instSFiniteRestrict

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

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

← MathLib Explorer

English

If μ is s-finite, then its restriction to any set s is s-finite: μ.restrict s is s-finite.

Русский

Если μ — s-finite, то ограничение μ на произвольное множество s также s-finite.

LaTeX

$$SFinite (μ.restrict s)$$

Lean4

instance [SFinite μ] (s : Set α) : SFinite (μ.restrict s) :=
  ⟨fun n ↦ (sfiniteSeq μ n).restrict s, fun n ↦ inferInstance, by rw [← restrict_sum_of_countable, sum_sfiniteSeq]⟩

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

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

Разделы

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

Аффилиация

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