neg — Mathlib

English

Analyticity is preserved under negation for constant functions.

Русский

Аналитичность сохраняется при отрицании константной функции.

LaTeX

$$$AnalyticAt\\ 𝕜 f x \\Rightarrow AnalyticAt\\ 𝕜 (-f) x$$$

Lean4

theorem neg (hf : HasFPowerSeriesWithinOnBall f pf s x r) : HasFPowerSeriesWithinOnBall (-f) (-pf) s x r :=
  { r_le := by
      rw [pf.radius_neg]
      exact hf.r_le
    r_pos := hf.r_pos
    hasSum := fun hy h'y => (hf.hasSum hy h'y).neg }

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