const_smul — Mathlib

English

If HasFPowerSeriesWithinOnBall f pf s x r, then HasFPowerSeriesWithinOnBall (c • f) (c • pf) s x r.

Русский

Если имеет место локальное разложение внутри шара, то c·f имеет разложение с pf масштабированным на c внутри того же шара.

LaTeX

$$$\text{HasFPowerSeriesWithinOnBall}(f, pf, s, x, r) \Rightarrow \text{HasFPowerSeriesWithinOnBall}(c \cdot f, c \cdot pf, s, x, r)$$$

Lean4

theorem const_smul (hf : HasFPowerSeriesWithinOnBall f pf s x r) : HasFPowerSeriesWithinOnBall (c • f) (c • pf) s x r
    where
  r_le := le_trans hf.r_le pf.radius_le_smul
  r_pos := hf.r_pos
  hasSum := fun hy h'y => (hf.hasSum hy h'y).const_smul _

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