English
For each natural number n, the family of intervals Iio(k+1) with k ∈ ℕ forms a finite spanning family for the additive Haar measure volumeIoiPow(n) on the open ray (0, ∞). In particular, these sets cover the entire ray and each chosen interval has finite volume.
Русский
Для каждого натурального числа n множество интервалов Iio(k+1) при k ∈ ℕ образуют конечное базисное порождающее семейство для плотной меры volumeIoiPow(n) на открытый луч (0, ∞). Другими словами, объединение этих множеств покрывает весь луч и каждой области соответствует конечный объем.
LaTeX
$$$\text{FiniteSpanningSetsIn}(\mathrm{volumeIoiPow}(n))\ (\mathrm{range}\ Iio).$$$
Lean4
/-- The intervals `(0, k + 1)` have finite measure `MeasureTheory.Measure.volumeIoiPow _`
and cover the whole open ray `(0, +∞)`. -/
def finiteSpanningSetsIn_volumeIoiPow_range_Iio (n : ℕ) : FiniteSpanningSetsIn (volumeIoiPow n) (range Iio)
where
set k := Iio ⟨k + 1, mem_Ioi.2 k.cast_add_one_pos⟩
set_mem _ := mem_range_self _
finite k := by simp [volumeIoiPow_apply_Iio]
spanning := iUnion_eq_univ_iff.2 fun x ↦ ⟨⌊x.1⌋₊, Nat.lt_floor_add_one x.1⟩
