smul_const — Mathlib

English

If ContinuousMul holds for two topologies t1 and t2 on M, then it also holds for t1 ⊓ t2.

Русский

Если умножение непрерывно в топологиях t1 и t2, то непрерывно и в их пересечении t1 ⊓ t2.

LaTeX

$$$\\text{ContinuousMul}$ на $t_1 \\inf t_2$$$

Lean4

@[to_additive]
theorem smul_const {f : α → M} {l : Filter α} {c : M} (hf : Tendsto f l (𝓝 c)) (a : X) :
    Tendsto (fun x => f x • a) l (𝓝 (c • a)) :=
  hf.smul tendsto_const_nhds

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