const_smul — Mathlib

English

If g is continuous within a set s at a point b, then for any fixed scalar c, the function x ↦ c • g(x) is also continuous within s at b.

Русский

Если g непрерывна внутри множества s в точке b, то для любого фиксированного скаляра c функция x ↦ c • g(x) тоже непрерывна внутри s в b.

LaTeX

$$$\text{ContinuousWithinAt } g\ s\ b \Rightarrow \forall c,\ \text{ContinuousWithinAt } (\lambda x. c \cdot g(x))\ s\ b.$$$

Lean4

@[to_additive]
nonrec theorem const_smul (hg : ContinuousWithinAt g s b) (c : M) : ContinuousWithinAt (fun x => c • g x) s b :=
  hg.const_smul c

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