spanningSets — Mathlib

English

If μ is σ-finite, then spanningSets μ is monotone in i.

Русский

Если μ σ-покрывает, то spanningSets μ образует монотонную последовательность.

LaTeX

$$Monotone (spanningSets μ)$$

Lean4

/-- A noncomputable way to get a monotone collection of sets that span `univ` and have finite
  measure using `Classical.choose`. This definition satisfies monotonicity in addition to all other
  properties in `SigmaFinite`. -/
def spanningSets (μ : Measure α) [SigmaFinite μ] (i : ℕ) : Set α :=
  Accumulate μ.toFiniteSpanningSetsIn.set i

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