spanningSets_mono

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

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

English

For μ σ-finite, if m ≤ n as natural numbers, then spanningSets μ m ⊆ spanningSets μ n.

Русский

Для μ σ-конечной, если m ≤ n, то spanningSets μ m ⊆ spanningSets μ n.

LaTeX

$$spanningSets μ m ⊆ spanningSets μ n$$

Lean4

@[gcongr]
theorem spanningSets_mono [SigmaFinite μ] {m n : ℕ} (hmn : m ≤ n) : spanningSets μ m ⊆ spanningSets μ n :=
  monotone_spanningSets _ hmn

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

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

Разделы

Аффилиация

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