eventually — Mathlib

English

Two power-series representations on the ball coincide on the ball.

Русский

Две представления степенного ряда на шаре совпадают на шаре.

LaTeX

$$$HasFPowerSeriesOnBall\ f p x r \Rightarrow HasFPowerSeriesOnBall\ g p x r \Rightarrow (EMetric.ball x r).EqOn\ f\ g$$$

Lean4

protected theorem eventually (hf : HasFPowerSeriesWithinAt f p s x) :
    ∀ᶠ r : ℝ≥0∞ in 𝓝[>] 0, HasFPowerSeriesWithinOnBall f p s x r :=
  let ⟨_, hr⟩ := hf
  mem_of_superset (Ioo_mem_nhdsGT hr.r_pos) fun _ hr' => hr.of_le hr'.1 hr'.2.le

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