hasFPowerSeriesWithinOnBall — Mathlib

English

If HasFPowerSeriesWithinAt f p s x holds and t ⊆ s relative to nhdsWithin, then it holds for t as well.

Русский

Если HasFPowerSeriesWithinAt для множества s вокруг x, и t ⊆ s в nhdsWithin, тогда это верно и для t.

LaTeX

$$$HasFPowerSeriesWithinAt f p s x \\to (t \\subset s) \\Rightarrow HasFPowerSeriesWithinAt f p t x$$$

Lean4

theorem hasFPowerSeriesWithinOnBall (hf : HasFPowerSeriesOnBall f p x r) : HasFPowerSeriesWithinOnBall f p s x r :=
  by
  rw [← hasFPowerSeriesWithinOnBall_univ] at hf
  exact hf.mono (subset_univ _)

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