const_smul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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