continuousAt_const_smul_iff — Mathlib

English

For any c ∈ G, ContinuousAt (c • f) at b is equivalent to ContinuousAt f at b.

Русский

Для любого c ∈ G непрерывность в точке для c • f равна непрерывности в точке для f.

LaTeX

$$$ \\mathrm{ContinuousAt}(\\lambda x. c \\cdot f(x))\\, b \\Leftrightarrow \\mathrm{ContinuousAt}(f)\\, b $$$

Lean4

@[to_additive]
theorem continuousAt_const_smul_iff (c : G) : ContinuousAt (fun x => c • f x) b ↔ ContinuousAt f b :=
  tendsto_const_smul_iff c

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