Theorems · Theorem · functional analysis

Bornology.isVonNBounded_iff_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],
  Filter.Tendsto ε l (nhdsWithin 0 {0}ᶜ) →
    ∀ {S : Set E}, Bornology.IsVonNBounded 𝕜 S ↔ ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Filter.Tendsto (ε • x) l (nhds 0)

Given any sequence ε of scalars which tends to 𝓝[≠] 0, we have that a set S is bounded if and only if for any sequence x : ℕ → S, ε • x tends to 0. This actually works for any indexing type ι, but in the special case ι = ℕ we get the important fact that convergent sequences fully characterize bounded sets.

Defined in

Mathlib.Analysis.LocallyConvex.Bounded

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldAddCommGroupModuleTopologicalSpaceContinuousSMulFilter.NeBot