English
The membership of an element in a union of sets described by approxOrderOf is equivalent to the existence of indices identifying membership in each component.
Русский
Членство элемента в объединении множеств, задаваемых через approxOrderOf, эквивалентно существованию индексов, определяющих принадлежность в каждом компоненте.
LaTeX
$$$$ a \in \bigcup_{i} s_{i} \iff \exists i, a \in s_{i}. $$$$
Lean4
/-- In a seminormed group `A`, given a sequence of distances `δ₁, δ₂, ...`, `wellApproximable A δ`
is the limsup as `n → ∞` of the sets `approxOrderOf A n δₙ`. Thus, it is the set of points that
lie in infinitely many of the sets `approxOrderOf A n δₙ`. -/
@[to_additive addWellApproximable /-- In a seminormed additive group `A`, given a sequence of
distances `δ₁, δ₂, ...`, `addWellApproximable A δ` is the limsup as `n → ∞` of the sets
`approxAddOrderOf A n δₙ`. Thus, it is the set of points that lie in infinitely many of the sets
`approxAddOrderOf A n δₙ`. -/
]
def wellApproximable (A : Type*) [SeminormedGroup A] (δ : ℕ → ℝ) : Set A :=
blimsup (fun n => approxOrderOf A n (δ n)) atTop fun n => 0 < n
