English
Definition: sigmaFiniteSetGE(μ, ν, n) is the witness t given by exists_isSigmaFiniteSet_measure_ge, i.e., a measurable t with μ|t sigma-finite and ν(t) bounded below by sup(ν over sigma-finite restrictions) minus 1/n.
Русский
Определение: sigmaFiniteSetGE(μ, ν, n) — показатель, задающий измеримое t, на котором μ|t сигма-конечно и ν(t) не меньше супрема ν над сигма-конечными ограничениями минус 1/n.
LaTeX
$$sigmaFiniteSetGE(μ,ν,n) := (exists_isSigmaFiniteSet_measure_ge μ ν n).choose$$
Lean4
/-- A measurable set such that `μ.restrict (μ.sigmaFiniteSetGE ν n)` is sigma-finite and
for `C` the supremum of `ν s` over all measurable sets `s` with `μ.restrict s` sigma-finite,
`ν (μ.sigmaFiniteSetGE ν n) ≥ C - 1/n`. -/
def sigmaFiniteSetGE (μ ν : Measure α) [IsFiniteMeasure ν] (n : ℕ) : Set α :=
(exists_isSigmaFiniteSet_measure_ge μ ν n).choose
