English
Let v be a Vitali family for a measure μ, and f a family of sets assigned to points. A subfamily on a set s is fine if for every x in s and every ε > 0 there exists t in v.setsAt(x) ∩ f(x) with t ⊆ closedBall(x, ε).
Русский
Пусть v — семейство Витали для мере μ, а f — семейство множеств, зависящее от точки. Подсемейство на множество s называется тонким, если для каждого x ∈ s и каждого ε > 0 существует множество t, принадлежащее v.setsAt(x) ∩ f(x), такое что t ⊆ замкнутый шар вокруг x радиуса ε.
LaTeX
$$$FineSubfamilyOn(v,f,s) \\iff \\forall x\\in s\\,\\forall \\varepsilon>0\\,\\exists t\\in v.setsAt(x)\\cap f(x),\\ t\\subseteq \\overline{B}(x,\\varepsilon).$$$
Lean4
/-- Given a Vitali family `v` for a measure `μ`, a family `f` is a fine subfamily on a set `s` if
every point `x` in `s` belongs to arbitrarily small sets in `v.setsAt x ∩ f x`. This is precisely
the subfamilies for which the Vitali family definition ensures that one can extract a disjoint
covering of almost all `s`. -/
def FineSubfamilyOn (v : VitaliFamily μ) (f : X → Set (Set X)) (s : Set X) : Prop :=
∀ x ∈ s, ∀ ε > 0, ∃ t ∈ v.setsAt x ∩ f x, t ⊆ closedBall x ε
