mem_wellApproximable_iff — Mathlib

English

For any A, δ, a, membership in wellApproximable(A, δ) is equivalent to membership in the limsup blimsup of approxOrderOf(A, n, δ(n)).

Русский

Для любых A, δ и a принадлежность a к wellApproximable(A, δ) эквивалентна принадлежности к limsup от approxOrderOf(A, n, δ(n)).

LaTeX

$$$$ a \in wellApproximable(A, δ) \iff a \in \mathrm{blimsup}_{n\to\infty} (\operatorname{approxOrderOf}(A, n, δ(n))) . $$$$

Lean4

@[to_additive mem_add_wellApproximable_iff]
theorem mem_wellApproximable_iff {A : Type*} [SeminormedGroup A] {δ : ℕ → ℝ} {a : A} :
    a ∈ wellApproximable A δ ↔ a ∈ blimsup (fun n => approxOrderOf A n (δ n)) atTop fun n => 0 < n :=
  Iff.rfl

Похожие утверждения