continuousWithinAt_const_smul_iff

English

For a fixed c ∈ G, ContinuousWithinAt (c • f) on s at b is equivalent to ContinuousWithinAt f on s at b.

Русский

Для фиксированного c ∈ G непрерывность внутри множества для c • f равна непрерывности внутри множества для f.

LaTeX

$$$ \\text{ContinuousWithinAt}(\\lambda x. c \\cdot f(x))\\, s\\, b \\Leftrightarrow \\ \\text{ContinuousWithinAt}(f) \\ s \\ b $$$

Lean4

@[to_additive]
theorem continuousWithinAt_const_smul_iff (c : G) :
    ContinuousWithinAt (fun x => c • f x) s b ↔ ContinuousWithinAt f s b :=
  tendsto_const_smul_iff c

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