continuousAt_const_smul_iff — Mathlib

English

For a unit c, ContinuousAt (λ x, c • f x) b is equivalent to ContinuousAt f b.

Русский

Для единицы c непрерывность в точке b сохраняется под умножением: ContinuousAt(λ x, c • f x) b эквивалентно ContinuousAt f b.

LaTeX

$$$ContinuousAt (\lambda x => c \cdot f x) b \iff ContinuousAt f b$$$

Lean4

nonrec theorem continuousAt_const_smul_iff (hc : IsUnit c) : ContinuousAt (fun x => c • f x) b ↔ ContinuousAt f b :=
  continuousAt_const_smul_iff hc.unit

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