Theorems · Theorem · functional analysis

Bornology.isVonNBounded_of_smul_tendsto_zero

∀ {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] {ε : ι → 𝕜} {l : Filter ι} [l.NeBot],
  (∀ᶠ (n : ι) in l, ε n ≠ 0) →
    ∀ {S : Set E},
      (∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Filter.Tendsto (ε • x) l (nhds 0)) → Bornology.IsVonNBounded 𝕜 S

Defined in

Mathlib.Analysis.LocallyConvex.Bounded

Cited by

2 results in Mathlib

Foundations

Depth 124 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldAddCommGroupModuleTopologicalSpaceContinuousSMulFilter.NeBot