finiteSpanningSetsInIooRat — Mathlib

English

For a locally finite measure μ on ℝ, the open intervals with rational endpoints can be spanned by a finite family; specifically, the sets Ioo(−(n+1), n+1) for n ∈ ℕ form a finite spanning family for the union of all rational-endpoint open intervals.

Русский

Для локально конечной меры μ на ℝ открытые интервалы с рациональными концами можно охватить конечной семейством; в частности, множества Ioo(−(n+1), n+1) при n∈ℕ образуют конечное порождающее семейство для объединения всех интервалов Ioo(a,b) с рациональными концами.

LaTeX

$$$$\mu \text{ locally finite} \Rightarrow \mu.FiniteSpanningSetsIn\Big(\bigcup_{a,b \in \mathbb{Q}, a

Lean4

/-- The intervals `(-(n + 1), (n + 1))` form a finite spanning sets in the set of open intervals
with rational endpoints for a locally finite measure `μ` on `ℝ`. -/
def finiteSpanningSetsInIooRat (μ : Measure ℝ) [IsLocallyFiniteMeasure μ] :
    μ.FiniteSpanningSetsIn (⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo (a : ℝ) (b : ℝ)})
    where
  set n := Ioo (-(n + 1)) (n + 1)
  set_mem
    n := by
    simp only [mem_iUnion, mem_singleton_iff]
    refine
      ⟨-(n + 1 : ℕ), n + 1, ?_, by simp⟩
        -- TODO: norm_cast fails here?

    push_cast
    exact neg_lt_self n.cast_add_one_pos
  finite _ := measure_Ioo_lt_top
  spanning :=
    iUnion_eq_univ_iff.2 fun x =>
      ⟨⌊|x|⌋₊, neg_lt.1 ((neg_le_abs x).trans_lt (Nat.lt_floor_add_one _)),
        (le_abs_self x).trans_lt (Nat.lt_floor_add_one _)⟩

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