English
If for every x ∈ X a family f x of subsets is frequently present in the filter v.filterAt x, then there is a FineSubfamilyOn f on a given set s; i.e., one can select, for each x ∈ s, a member t ∈ f x with t small enough (as ε → 0) to witness the subfamily.
Русский
Если для каждого x ∈ X семейство f x подмножеств часто встречается в фильтре v.filterAt x, то существует тонкая подподборка на множестве s; то есть для каждого x ∈ s выбирается множество t ∈ f x с малыми размерами.
LaTeX
$$$\\forall x \\in s, \\text{Frequently}(t \\in v.filterAt x, t \\in f x) \\Rightarrow v.FineSubfamilyOn f s$$$
Lean4
theorem fineSubfamilyOn_of_frequently (v : VitaliFamily μ) (f : X → Set (Set X)) (s : Set X)
(h : ∀ x ∈ s, ∃ᶠ t in v.filterAt x, t ∈ f x) : v.FineSubfamilyOn f s :=
by
intro x hx ε εpos
obtain ⟨t, tv, ht, tf⟩ : ∃ t ∈ v.setsAt x, t ⊆ closedBall x ε ∧ t ∈ f x := v.frequently_filterAt_iff.1 (h x hx) ε εpos
exact ⟨t, ⟨tv, tf⟩, ht⟩
