smul — Mathlib

English

If f is bounded along l, then c · f is bounded along l for any scalar c.

Русский

Если f ограничена вдоль l, то c · f ограничена вдоль l для любого скалярного c.

LaTeX

$$$\\forall c,\\ \\mathrm{BoundedAtFilter}(l,f) \\Rightarrow \\mathrm{BoundedAtFilter}(l, c \\cdot f)$$$

Lean4

theorem smul [SeminormedRing 𝕜] [SeminormedAddCommGroup β] [Module 𝕜 β] [IsBoundedSMul 𝕜 β] {l : Filter α} {f : α → β}
    (c : 𝕜) (hf : BoundedAtFilter l f) : BoundedAtFilter l (c • f) :=
  hf.const_smul_left c

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