English
Define wellApproximable(A, δ) as the limsup, as n → ∞, of the sets approxOrderOf(A, n, δ(n)). It is the set of points that lie in infinitely many of these sets.
Русский
Определим wellApproximable(A, δ) как предел по пределу (limsup) наборов approxOrderOf(A, n, δ(n)) при n → ∞: это множество точек, которые принадлежат бесконечно многим из этих множеств.
LaTeX
$$$$ wellApproximable(A, δ) = \operatorname{blimsup}_{n\to\infty} (\operatorname{approxOrderOf}(A, n, δ(n))). $$$$
Lean4
/-- In a seminormed group `A`, given `n : ℕ` and `δ : ℝ`, `approxOrderOf A n δ` is the set of
elements within a distance `δ` of a point of order `n`. -/
@[to_additive /-- In a seminormed additive group `A`, given `n : ℕ` and `δ : ℝ`,
`approxAddOrderOf A n δ` is the set of elements within a distance `δ` of a point of order `n`. -/
]
def approxOrderOf (A : Type*) [SeminormedGroup A] (n : ℕ) (δ : ℝ) : Set A :=
thickening δ {y | orderOf y = n}
