English
Let v be a Vitali family on a metric space X. For a point x ∈ X and a property P on subsets of X, P holds for frequently many sets t in the filter v.filterAt x if and only if for every radius ε > 0 there exists a set t ∈ v.setsAt x with t ⊆ the closed ball around x of radius ε and P t holds.
Русский
Пусть v — семейство Витали на метрическом пространстве X. Для точки x ∈ X и свойства P над подмножествами X, P выполняется для часто встречающихся множеств t в фильтре v.filterAt x тогда и только тогда, когда для любого радиуса ε > 0 найдется множество t ∈ v.setsAt x такое, что t ⊆ замкнутого шара B̄(x, ε) и P t выполняется.
LaTeX
$$$(\\exists^{\\mathrm{freq}} t \\in v.filterAt x, P t) \\iff \\forall \\varepsilon > 0, \\exists t \\in v.setsAt x, t \\subseteq \\overline{B}(x, \\varepsilon) \\wedge P t$$$
Lean4
theorem frequently_filterAt_iff {x : X} {P : Set X → Prop} :
(∃ᶠ t in v.filterAt x, P t) ↔ ∀ ε > (0 : ℝ), ∃ t ∈ v.setsAt x, t ⊆ closedBall x ε ∧ P t := by
simp only [(v.filterAt_basis_closedBall x).frequently_iff, ← and_assoc, subset_def, mem_setOf]
