sigmaFinite_of_le

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

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

English

If μ is sigma-finite and ν ≤ μ, then ν is sigma-finite.

Русский

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

LaTeX

$$$(μ : Measure α) [hs : SigmaFinite μ] (h : ν ≤ μ) : SigmaFinite ν$$$

Lean4

theorem sigmaFinite_of_le (μ : Measure α) [hs : SigmaFinite μ] (h : ν ≤ μ) : SigmaFinite ν :=
  ⟨hs.out.map <| FiniteSpanningSetsIn.ofLE h⟩

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

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

Разделы

Аффилиация

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