instSigmaFiniteRestrictInterSet

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

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

← MathLib Explorer

English

If μ and ν are sigma-finite, then μ + ν is sigma-finite.

Русский

Если μ и ν сигма-конечны, то μ + ν сигма-конечна.

LaTeX

$$instance sigmaFinite (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] : SigmaFinite (instHAdd.hAdd μ ν)$$

Lean4

instance [SigmaFinite (μ.restrict s)] : SigmaFinite (μ.restrict (s ∩ t)) :=
  sigmaFinite_of_le (μ.restrict s) (restrict_mono_ae (ae_of_all _ Set.inter_subset_left))

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

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

Разделы

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

Аффилиация

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