hasFPowerSeriesWithinAt_univ — Mathlib

English

The equivalence between HasFPowerSeriesWithinOnBall on universal set and HasFPowerSeriesOnBall holds.

Русский

Эквивалентность между HasFPowerSeriesWithinOnBall на все множество и HasFPowerSeriesOnBall.

LaTeX

$$$HasFPowerSeriesWithinOnBall f p f Set.univ x r \\iff HasFPowerSeriesOnBall f p x r$$$

Lean4

@[simp]
theorem hasFPowerSeriesWithinAt_univ : HasFPowerSeriesWithinAt f p univ x ↔ HasFPowerSeriesAt f p x := by
  simp only [HasFPowerSeriesWithinAt, hasFPowerSeriesWithinOnBall_univ, HasFPowerSeriesAt]

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