eventually — Mathlib

English

There exists a neighborhood of radii r > 0 such that HasFiniteFPowerSeriesOnBall f p x n r holds for all r in that neighborhood.

Русский

Существует окрестность радиусов r > 0, внутри которой справедливо HasFiniteFPowerSeriesOnBall f p x n r для всех таких r.

LaTeX

$$$\forall hf : HasFiniteFPowerSeriesAt f p x n,\ ∀ᶠ r \in 𝓝[>0], HasFiniteFPowerSeriesOnBall f p x n r.$$$

Lean4

protected theorem eventually (hf : HasFiniteFPowerSeriesAt f p x n) :
    ∀ᶠ r : ℝ≥0∞ in 𝓝[>] 0, HasFiniteFPowerSeriesOnBall f p x n r :=
  hf.hasFPowerSeriesAt.eventually.mono fun _ h ↦ ⟨h, hf.finite⟩

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