English
If f has a finite power series on a ball of radius r with order n, and r′ is a smaller positive radius (0 < r′ ≤ r), then f also has a finite power series on the ball of radius r′ with the same order n.
Русский
Если у функции f есть конечный степенной ряд на шаре радиуса r с порядком n, и r′ является меньшим положительным радиусом (0 < r′ ≤ r), тогда у f тоже есть конечный степенной ряд на шаре радиуса r′ с тем же порядком n.
LaTeX
$$$HasFiniteFPowerSeriesOnBall\ f\ p\ x\ n\ r \land 0 < r'\land r' \le r \Rightarrow HasFiniteFPowerSeriesOnBall\ f\ p\ x\ n\ r'.$$$
Lean4
theorem mono (hf : HasFiniteFPowerSeriesOnBall f p x n r) (r'_pos : 0 < r') (hr : r' ≤ r) :
HasFiniteFPowerSeriesOnBall f p x n r' :=
⟨hf.1.mono r'_pos hr, hf.finite⟩
