smul — Mathlib

English

If a family ts of topologies on M has the property that each ts i yields continuous multiplication, then the infimum topology across the range also yields continuous multiplication.

Русский

Если у семейства топологий ts на M каждая делает умножение непрерывным, то их пересечение по диапазону также делает умножение непрерывным.

LaTeX

$$$\\text{ContinuousMul}$ на $\\bigwedge i, ts_i$$$

Lean4

@[to_additive]
theorem smul {f : α → M} {g : α → X} {l : Filter α} {c : M} {a : X} (hf : Tendsto f l (𝓝 c)) (hg : Tendsto g l (𝓝 a)) :
    Tendsto (fun x => f x • g x) l (𝓝 <| c • a) :=
  (continuous_smul.tendsto _).comp (hf.prodMk_nhds hg)

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