sigmaFiniteSet — Mathlib

English

μ.sigmaFiniteSetWRT' ν equals the union of μ.sigmaFiniteSetGE ν n over n, and ν of that equals the supremum over s of ν(s) with SigmaFinite μ|s.

Русский

μ.sigmaFiniteSetWRT' ν равняется объединению μ.sigmaFiniteSetGE ν n по всем n; мера ν этого равна supremum ν(s) по всем s, где μ|s сигма-финитна.

LaTeX

$$$$\mu.sigmaFiniteSetWRT'(\nu) = \bigcup_{n} \mu.sigmaFiniteSetGE(\nu, n),\quad \nu(\mu.sigmaFiniteSetWRT'(\nu)) = \bigvee_{s:\text{MeasurableSet},\ \SigmaFinite(\mu\restriction s)} \nu(s).$$$$

Lean4

/-- A measurable set such that `μ.restrict μ.sigmaFiniteSet` is sigma-finite,
  and for all measurable sets `s ⊆ μ.sigmaFiniteSetᶜ`, either `μ s = 0` or `μ s = ∞`. -/
def sigmaFiniteSet (μ : Measure α) : Set α :=
  μ.sigmaFiniteSetWRT μ

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