Theorems · Definition · number theory

wellApproximable

(A : Type u_1) → [SeminormedGroup A] → (ℕ → ℝ) → Set A

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 δₙ.

Defined in

Mathlib.NumberTheory.WellApproximable

Cited by

1 results in Mathlib

Foundations

Depth 150 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedGroup