English
If s is null-measurable with finite volume, and s lies inside the π-volume space, then the set {ν : box n ν ⊆ s} is finite.
Русский
Если s обычной меры нуль и имеет конечный объём, и s содержит box-кубы, тогда множество ν, для которых box n ν ⊆ s, конечно конечное.
LaTeX
$$Set.Finite {ν : ι → ℤ | box(n,ν) ⊆ s}$$
Lean4
theorem setFinite_index {s : Set (ι → ℝ)} (hs₁ : NullMeasurableSet s) (hs₂ : volume s ≠ ⊤) :
Set.Finite {ν : ι → ℤ | ↑(box n ν) ⊆ s} :=
by
refine
(Measure.finite_const_le_meas_of_disjoint_iUnion₀ volume (ε := 1 / n ^ card ι) (by simp) (As := fun ν : ι → ℤ ↦
(box n ν) ∩ s) (fun ν ↦ ?_) (fun _ _ h ↦ ?_) ?_).subset
(fun _ hν ↦ ?_)
· refine NullMeasurableSet.inter ?_ hs₁
exact (box n ν).measurableSet_coe.nullMeasurableSet
· exact ((Disjoint.inter_right _ (disjoint.mp h)).inter_left _).aedisjoint
·
exact
lt_top_iff_ne_top.mp <|
measure_lt_top_of_subset (by simp only [Set.iUnion_subset_iff, Set.inter_subset_right, implies_true]) hs₂
· rw [Set.mem_setOf, Set.inter_eq_self_of_subset_left hν, volume_box]
