smul_tendsto_zero — Mathlib

English

If S is VN bounded, nbhds of 0 absorb S and scalar multiples converge to 0 along any tending scalar sequence.

Русский

VN ограниченность сохраняется под скалярным умножением, если скаляр стремится к нулю.

LaTeX

$$hS : IsVonNBounded 𝕜 S → ∀ᶠ n in l, x n ∈ S → Tendsto ε l (𝓝 0) → Tendsto (ε • x) l (nhds 0)$$

Lean4

theorem smul_tendsto_zero [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {S : Set E} {ε : ι → 𝕜}
    {x : ι → E} {l : Filter ι} (hS : IsVonNBounded 𝕜 S) (hxS : ∀ᶠ n in l, x n ∈ S) (hε : Tendsto ε l (𝓝 0)) :
    Tendsto (ε • x) l (𝓝 0) :=
  (hS.tendsto_smallSets_nhds.comp hε).of_smallSets <| hxS.mono fun _ ↦ smul_mem_smul_set

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