# Von Neumann Boundedness #

This file defines natural or von Neumann bounded sets and proves elementary properties.

## Main declarations #

- `Bornology.IsVonNBounded`: A set `s` is von Neumann-bounded if every neighborhood of zero absorbs `s`.
- `Bornology.vonNBornology`: The bornology made of the von Neumann-bounded sets.

## Main results #

- `Bornology.IsVonNBounded.of_topologicalSpace_le`: A coarser topology admits more von Neumann-bounded sets.
- `Bornology.IsVonNBounded.image`: A continuous linear image of a bounded set is bounded.
- `Bornology.isVonNBounded_iff_smul_tendsto_zero`: 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 shows that bounded sets are completely determined by sequences, which is the key fact for proving that sequential continuity implies continuity for linear maps defined on a bornological space

## References #

- [Bourbaki, Topological Vector Spaces][bourbaki1987]

source
def Bornology.IsVonNBounded (𝕜 : Type u_1) {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] (s : Set E) :
Prop

A set `s` is von Neumann bounded if every neighborhood of 0 absorbs `s`.

Equations

- Bornology.IsVonNBounded 𝕜 s = ∀ ⦃V : Set E⦄, V ∈ nhds 0 → Absorbs 𝕜 V s

Instances For

source
@[simp]
theorem Bornology.isVonNBounded_empty (𝕜 : Type u_1) (E : Type u_3) [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] :
IsVonNBounded 𝕜 ∅
source
theorem Bornology.isVonNBounded_iff {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] (s : Set E) :
IsVonNBounded 𝕜 s ↔ ∀ V ∈ nhds 0, Absorbs 𝕜 V s
source
theorem Filter.HasBasis.isVonNBounded_iff {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_5} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] {q : ι → Prop} {s : ι → Set E} {A : Set E} (h : (nhds 0).HasBasis q s) :
Bornology.IsVonNBounded 𝕜 A ↔ ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
source
theorem Bornology.IsVonNBounded.subset {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] {s₁ s₂ : Set E} (h : s₁ ⊆ s₂) (hs₂ : IsVonNBounded 𝕜 s₂) :
IsVonNBounded 𝕜 s₁

Subsets of bounded sets are bounded.

source
@[simp]
theorem Bornology.isVonNBounded_union {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] {s t : Set E} :
IsVonNBounded 𝕜 (s ∪ t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
source
theorem Bornology.IsVonNBounded.union {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] {s₁ s₂ : Set E} (hs₁ : IsVonNBounded 𝕜 s₁) (hs₂ : IsVonNBounded 𝕜 s₂) :
IsVonNBounded 𝕜 (s₁ ∪ s₂)

The union of two bounded sets is bounded.

source
theorem Bornology.IsVonNBounded.of_boundedSpace {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] [BoundedSpace 𝕜] {s : Set E} :
IsVonNBounded 𝕜 s
source
theorem Bornology.IsVonNBounded.of_subsingleton {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] [Subsingleton E] {s : Set E} :
IsVonNBounded 𝕜 s
source
@[simp]
theorem Bornology.isVonNBounded_iUnion {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] {ι : Sort u_6} [Finite ι] {s : ι → Set E} :
IsVonNBounded 𝕜 (⋃ (i : ι), s i) ↔ ∀ (i : ι), IsVonNBounded 𝕜 (s i)
source
theorem Bornology.isVonNBounded_biUnion {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] {ι : Type u_6} {I : Set ι} (hI : I.Finite) {s : ι → Set E} :
IsVonNBounded 𝕜 (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
source
theorem Bornology.isVonNBounded_sUnion {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] {S : Set (Set E)} (hS : S.Finite) :
IsVonNBounded 𝕜 (⋃₀ S) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s
source
theorem Bornology.IsVonNBounded.add {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [AddZeroClass E] [TopologicalSpace E] [ContinuousAdd E] [DistribSMul 𝕜 E] {s t : Set E} (hs : IsVonNBounded 𝕜 s) (ht : IsVonNBounded 𝕜 t) :
IsVonNBounded 𝕜 (s + t)
source
theorem Bornology.IsVonNBounded.neg {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [AddGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [DistribMulAction 𝕜 E] {s : Set E} (hs : IsVonNBounded 𝕜 s) :
IsVonNBounded 𝕜 (-s)
source
@[simp]
theorem Bornology.isVonNBounded_neg {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [AddGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [DistribMulAction 𝕜 E] {s : Set E} :
IsVonNBounded 𝕜 (-s) ↔ IsVonNBounded 𝕜 s
source
theorem Bornology.IsVonNBounded.of_neg {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [AddGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [DistribMulAction 𝕜 E] {s : Set E} :
IsVonNBounded 𝕜 (-s) → IsVonNBounded 𝕜 s

Alias of the forward direction of `Bornology.isVonNBounded_neg`.

source
theorem Bornology.IsVonNBounded.sub {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [AddGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [DistribMulAction 𝕜 E] {s t : Set E} (hs : IsVonNBounded 𝕜 s) (ht : IsVonNBounded 𝕜 t) :
IsVonNBounded 𝕜 (s - t)
source
theorem Bornology.IsVonNBounded.of_topologicalSpace_le {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {t t' : TopologicalSpace E} (h : t ≤ t') {s : Set E} (hs : IsVonNBounded 𝕜 s) :
IsVonNBounded 𝕜 s

If a topology `t'` is coarser than `t`, then any set `s` that is bounded with respect to `t` is bounded with respect to `t'`.

source
theorem Bornology.isVonNBounded_iff_tendsto_smallSets_nhds {𝕜 : Type u_6} {E : Type u_7} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {S : Set E} :
IsVonNBounded 𝕜 S ↔ Filter.Tendsto (fun (x : 𝕜) => x • S) (nhds 0) (nhds 0).smallSets
source
theorem Bornology.IsVonNBounded.tendsto_smallSets_nhds {𝕜 : Type u_6} {E : Type u_7} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {S : Set E} :
IsVonNBounded 𝕜 S → Filter.Tendsto (fun (x : 𝕜) => x • S) (nhds 0) (nhds 0).smallSets

Alias of the forward direction of `Bornology.isVonNBounded_iff_tendsto_smallSets_nhds`.

source
theorem Bornology.isVonNBounded_iff_absorbing_le {𝕜 : Type u_6} {E : Type u_7} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {S : Set E} :
IsVonNBounded 𝕜 S ↔ Filter.absorbing 𝕜 S ≤ nhds 0
source
theorem Bornology.isVonNBounded_pi_iff {𝕜 : Type u_6} {ι : Type u_7} {E : ι → Type u_8} [NormedDivisionRing 𝕜] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E i)] {S : Set ((i : ι) → E i)} :
IsVonNBounded 𝕜 S ↔ ∀ (i : ι), IsVonNBounded 𝕜 (Function.eval i '' S)
source
theorem Bornology.IsVonNBounded.image {E : Type u_3} {F : Type u_4} {𝕜₁ : Type u_6} {𝕜₂ : Type u_7} [NormedDivisionRing 𝕜₁] [NormedDivisionRing 𝕜₂] [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] {σ : 𝕜₁ →+* 𝕜₂} [RingHomSurjective σ] [RingHomIsometric σ] {s : Set E} (hs : IsVonNBounded 𝕜₁ s) (f : E →SL[σ] F) :
IsVonNBounded 𝕜₂ (⇑f '' s)

A continuous linear image of a bounded set is bounded.

source
theorem Bornology.IsVonNBounded.smul_tendsto_zero {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_5} [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ε : Filter.Tendsto ε l (nhds 0)) :
Filter.Tendsto (ε • x) l (nhds 0)
source
theorem Bornology.isVonNBounded_of_smul_tendsto_zero {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_5} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] {ε : ι → 𝕜} {l : Filter ι} [l.NeBot] (hε : ∀ᶠ (n : ι) in l, ε n ≠ 0) {S : Set E} (H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Filter.Tendsto (ε • x) l (nhds 0)) :
IsVonNBounded 𝕜 S
source
theorem Bornology.isVonNBounded_iff_smul_tendsto_zero {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_5} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] {ε : ι → 𝕜} {l : Filter ι} [l.NeBot] (hε : Filter.Tendsto ε l (nhdsWithin 0 {0}ᶜ)) {S : Set E} :
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.

source
theorem Bornology.IsVonNBounded.extend_scalars {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_6} [AddCommGroup E] [Module 𝕜 E] (𝕝 : Type u_7) [NontriviallyNormedField 𝕝] [NormedAlgebra 𝕜 𝕝] [Module 𝕝 E] [TopologicalSpace E] [ContinuousSMul 𝕝 E] [IsScalarTower 𝕜 𝕝 E] {s : Set E} (h : IsVonNBounded 𝕜 s) :
IsVonNBounded 𝕝 s

If a set is von Neumann bounded with respect to a smaller field, then it is also von Neumann bounded with respect to a larger field. See also `Bornology.IsVonNBounded.restrict_scalars` below.

source
theorem Bornology.isVonNBounded_singleton {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] (x : E) :
IsVonNBounded 𝕜 {x}

Singletons are bounded.

source
@[simp]
theorem Bornology.isVonNBounded_insert {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] (x : E) {s : Set E} :
IsVonNBounded 𝕜 (insert x s) ↔ IsVonNBounded 𝕜 s
source
theorem Bornology.IsVonNBounded.insert {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] (x : E) {s : Set E} :
IsVonNBounded 𝕜 s → IsVonNBounded 𝕜 (insert x s)

Alias of the reverse direction of `Bornology.isVonNBounded_insert`.

source
theorem Set.Finite.isVonNBounded {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] {s : Set E} (hs : s.Finite) :
Bornology.IsVonNBounded 𝕜 s

Finite sets are bounded.

source
theorem Bornology.IsVonNBounded.vadd {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s : Set E} (hs : IsVonNBounded 𝕜 s) (x : E) :
IsVonNBounded 𝕜 (x +ᵥ s)
source
@[simp]
theorem Bornology.isVonNBounded_vadd {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s : Set E} (x : E) :
IsVonNBounded 𝕜 (x +ᵥ s) ↔ IsVonNBounded 𝕜 s
source
theorem Bornology.IsVonNBounded.of_add_right {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s t : Set E} (hst : IsVonNBounded 𝕜 (s + t)) (hs : s.Nonempty) :
IsVonNBounded 𝕜 t
source
theorem Bornology.IsVonNBounded.of_add_left {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s t : Set E} (hst : IsVonNBounded 𝕜 (s + t)) (ht : t.Nonempty) :
IsVonNBounded 𝕜 s
source
theorem Bornology.isVonNBounded_add_of_nonempty {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s t : Set E} (hs : s.Nonempty) (ht : t.Nonempty) :
IsVonNBounded 𝕜 (s + t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
source
theorem Bornology.isVonNBounded_add {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s t : Set E} :
IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
source
@[simp]
theorem Bornology.isVonNBounded_add_self {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s : Set E} :
IsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s
source
theorem Bornology.IsVonNBounded.of_sub_left {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s t : Set E} (hst : IsVonNBounded 𝕜 (s - t)) (ht : t.Nonempty) :
IsVonNBounded 𝕜 s
source
theorem Bornology.IsVonNBounded.of_sub_right {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [IsTopologicalAddGroup E] {s t : Set E} (hst : IsVonNBounded 𝕜 (s - t)) (hs : s.Nonempty) :
IsVonNBounded 𝕜 t
source
theorem Bornology.isVonNBounded_sub_of_nonempty {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [IsTopologicalAddGroup E] {s t : Set E} (hs : s.Nonempty) (ht : t.Nonempty) :
IsVonNBounded 𝕜 (s - t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
source
theorem Bornology.isVonNBounded_sub {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [IsTopologicalAddGroup E] {s t : Set E} :
IsVonNBounded 𝕜 (s - t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
source
theorem Bornology.sUnion_isVonNBounded_eq_univ {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] :
⋃₀ setOf (IsVonNBounded 𝕜) = Set.univ

The union of all bounded set is the whole space.

source
@[deprecated Bornology.sUnion_isVonNBounded_eq_univ (since := "2025-11-14")]
theorem Bornology.isVonNBounded_covers {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] :
⋃₀ setOf (IsVonNBounded 𝕜) = Set.univ

Alias of `Bornology.sUnion_isVonNBounded_eq_univ`.

The union of all bounded set is the whole space.

source
@[reducible, inline]
abbrev Bornology.vonNBornology (𝕜 : Type u_1) (E : Type u_3) [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] :
Bornology E

The von Neumann bornology defined by the von Neumann bounded sets.

Note that this is not registered as an instance, in order to avoid diamonds with the metric bornology.

Equations

- Bornology.vonNBornology 𝕜 E = Bornology.ofBounded (setOf (Bornology.IsVonNBounded 𝕜)) ⋯ ⋯ ⋯ ⋯

Instances For

source
@[simp]
theorem Bornology.isBounded_iff_isVonNBounded (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] {s : Set E} :
IsBounded s ↔ IsVonNBounded 𝕜 s
source
theorem TotallyBounded.isVonNBounded (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜 E] {s : Set E} (hs : TotallyBounded s) :
Bornology.IsVonNBounded 𝕜 s
source
theorem Filter.Tendsto.isVonNBounded_range (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {f : ℕ → E} {x : E} (hf : Tendsto f atTop (nhds x)) :
Bornology.IsVonNBounded 𝕜 (Set.range f)
source
theorem Bornology.IsVonNBounded.restrict_scalars_of_nontrivial (𝕜 : Type u_1) {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜'] [Zero E] [TopologicalSpace E] [SMul 𝕜 E] [MulAction 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {s : Set E} (h : IsVonNBounded 𝕜' s) :
IsVonNBounded 𝕜 s
source
theorem Bornology.IsVonNBounded.restrict_scalars (𝕜 : Type u_1) {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Zero E] [TopologicalSpace E] [SMul 𝕜 E] [MulActionWithZero 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {s : Set E} (h : IsVonNBounded 𝕜' s) :
IsVonNBounded 𝕜 s
source
theorem NormedSpace.isVonNBounded_of_isBounded (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} (h : Bornology.IsBounded s) :
Bornology.IsVonNBounded 𝕜 s
source
theorem NormedSpace.isVonNBounded_ball (𝕜 : Type u_1) (E : Type u_3) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (r : ℝ) :
Bornology.IsVonNBounded 𝕜 (Metric.ball 0 r)
source
theorem NormedSpace.isVonNBounded_closedBall (𝕜 : Type u_1) (E : Type u_3) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (r : ℝ) :
Bornology.IsVonNBounded 𝕜 (Metric.closedBall 0 r)
source
theorem NormedSpace.isVonNBounded_iff (𝕜 : Type u_1) {E : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} :
Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s
source
theorem NormedSpace.isVonNBounded_iff' (𝕜 : Type u_1) {E : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} :
Bornology.IsVonNBounded 𝕜 s ↔ ∃ (r : ℝ), ∀ x ∈ s, ‖x‖ ≤ r
source
theorem NormedSpace.image_isVonNBounded_iff (𝕜 : Type u_1) {E : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {α : Type u_6} {f : α → E} {s : Set α} :
Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∃ (r : ℝ), ∀ x ∈ s, ‖f x‖ ≤ r
source
theorem NormedSpace.vonNBornology_eq (𝕜 : Type u_1) {E : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
Bornology.vonNBornology 𝕜 E = PseudoMetricSpace.toBornology

In a normed space, the von Neumann bornology (`Bornology.vonNBornology`) is equal to the metric bornology.

source
theorem NormedSpace.isBounded_iff_subset_smul_ball (𝕜 : Type u_1) {E : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} :
Bornology.IsBounded s ↔ ∃ (a : 𝕜), s ⊆ a • Metric.ball 0 1
source
theorem NormedSpace.isBounded_iff_subset_smul_closedBall (𝕜 : Type u_1) {E : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} :
Bornology.IsBounded s ↔ ∃ (a : 𝕜), s ⊆ a • Metric.closedBall 0 1
source
class QuasiCompleteSpace (𝕜 : Type u_6) (E : Type u_7) [Zero E] [UniformSpace E] [SeminormedRing 𝕜] [SMul 𝕜 E] :
Prop

A locally convex space is quasi-complete if every closed and von Neumann bounded set is complete.

- quasiComplete ⦃s : Set E⦄ : Bornology.IsVonNBounded 𝕜 s → IsClosed s → IsComplete s

  A locally convex space is quasi-complete if every closed and von Neumann bounded set is complete.

Instances

source
instance instQuasiCompleteSpaceOfCompleteSpace {𝕜 : Type u_6} {E : Type u_7} [Zero E] [UniformSpace E] [SeminormedRing 𝕜] [SMul 𝕜 E] [CompleteSpace E] :
QuasiCompleteSpace 𝕜 E

A complete space is quasi-complete with respect to any scalar ring.

source
theorem isCompact_closure_of_totallyBounded_quasiComplete {E : Type u_8} {𝕜 : Type u_9} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜 E] [QuasiCompleteSpace 𝕜 E] {s : Set E} (hs : TotallyBounded s) :
IsCompact (closure s)

[Bourbaki, Topological Vector Spaces, III §1.6][bourbaki1987]