# Algebraic facts about the topology of uniform convergence #

This file contains algebraic compatibility results about the uniform structure of uniform convergence / 𝔖-convergence. They will mostly be useful for defining strong topologies on the space of continuous linear maps between two topological vector spaces.

## Main statements #

• UniformFun.uniform_group : if G is a uniform group, then α →ᵤ G a uniform group
• UniformOnFun.uniform_group : if G is a uniform group, then for any 𝔖 : Set (Set α), α →ᵤ[𝔖] G a uniform group.
• UniformOnFun.continuousSMul_induced_of_image_bounded : let E be a TVS, 𝔖 : Set (Set α) and H a submodule of α →ᵤ[𝔖] E. If the image of any S ∈ 𝔖 by any u ∈ H is bounded (in the sense of Bornology.IsVonNBounded), then H, equipped with the topology induced from α →ᵤ[𝔖] E, is a TVS.

## Implementation notes #

Like in Topology/UniformSpace/UniformConvergenceTopology, we use the type aliases UniformFun (denoted α →ᵤ β) and UniformOnFun (denoted α →ᵤ[𝔖] β) for functions from α to β endowed with the structures of uniform convergence and 𝔖-convergence.

## References #

• [N. Bourbaki, General Topology, Chapter X][bourbaki1966]
• [N. Bourbaki, Topological Vector Spaces][bourbaki1987]

## Tags #

uniform convergence, strong dual

instance instZeroUniformFun {α : Type u_1} {β : Type u_2} [Zero β] :
Zero ()
Equations
• instZeroUniformFun = Pi.instZero
instance instOneUniformFun {α : Type u_1} {β : Type u_2} [One β] :
One ()
Equations
• instOneUniformFun = Pi.instOne
@[simp]
theorem UniformFun.toFun_zero {α : Type u_1} {β : Type u_2} [Zero β] :
UniformFun.toFun 0 = 0
@[simp]
theorem UniformFun.toFun_one {α : Type u_1} {β : Type u_2} [One β] :
UniformFun.toFun 1 = 1
@[simp]
theorem UniformFun.ofFun_zero {α : Type u_1} {β : Type u_2} [Zero β] :
UniformFun.ofFun 0 = 0
@[simp]
theorem UniformFun.ofFun_one {α : Type u_1} {β : Type u_2} [One β] :
UniformFun.ofFun 1 = 1
instance instZeroUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Zero β] :
Zero (UniformOnFun α β 𝔖)
Equations
• instZeroUniformOnFun = Pi.instZero
instance instOneUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [One β] :
One (UniformOnFun α β 𝔖)
Equations
• instOneUniformOnFun = Pi.instOne
@[simp]
theorem UniformOnFun.toFun_zero {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Zero β] :
0 = 0
@[simp]
theorem UniformOnFun.toFun_one {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [One β] :
1 = 1
@[simp]
theorem UniformOnFun.zero_apply {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Zero β] :
0 = 0
@[simp]
theorem UniformOnFun.one_apply {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [One β] :
1 = 1
instance instAddUniformFun {α : Type u_1} {β : Type u_2} [Add β] :
Equations
instance instMulUniformFun {α : Type u_1} {β : Type u_2} [Mul β] :
Mul ()
Equations
• instMulUniformFun = Pi.instMul
@[simp]
theorem UniformFun.toFun_add {α : Type u_1} {β : Type u_2} [Add β] (f : ) (g : ) :
UniformFun.toFun (f + g) = UniformFun.toFun f + UniformFun.toFun g
@[simp]
theorem UniformFun.toFun_mul {α : Type u_1} {β : Type u_2} [Mul β] (f : ) (g : ) :
UniformFun.toFun (f * g) = UniformFun.toFun f * UniformFun.toFun g
@[simp]
theorem UniformFun.ofFun_add {α : Type u_1} {β : Type u_2} [Add β] (f : αβ) (g : αβ) :
UniformFun.ofFun (f + g) = UniformFun.ofFun f + UniformFun.ofFun g
@[simp]
theorem UniformFun.ofFun_mul {α : Type u_1} {β : Type u_2} [Mul β] (f : αβ) (g : αβ) :
UniformFun.ofFun (f * g) = UniformFun.ofFun f * UniformFun.ofFun g
instance instAddUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Add β] :
Equations
instance instMulUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Mul β] :
Mul (UniformOnFun α β 𝔖)
Equations
• instMulUniformOnFun = Pi.instMul
@[simp]
theorem UniformOnFun.toFun_add {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Add β] (f : UniformOnFun α β 𝔖) (g : UniformOnFun α β 𝔖) :
(f + g) = f + g
@[simp]
theorem UniformOnFun.toFun_mul {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Mul β] (f : UniformOnFun α β 𝔖) (g : UniformOnFun α β 𝔖) :
(f * g) = f * g
@[simp]
theorem UniformOnFun.ofFun_add {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Add β] (f : αβ) (g : αβ) :
(f + g) = f + g
@[simp]
theorem UniformOnFun.ofFun_mul {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Mul β] (f : αβ) (g : αβ) :
(f * g) = f * g
instance instNegUniformFun {α : Type u_1} {β : Type u_2} [Neg β] :
Neg ()
Equations
• instNegUniformFun = Pi.instNeg
instance instInvUniformFun {α : Type u_1} {β : Type u_2} [Inv β] :
Inv ()
Equations
• instInvUniformFun = Pi.instInv
@[simp]
theorem UniformFun.toFun_neg {α : Type u_1} {β : Type u_2} [Neg β] (f : ) :
UniformFun.toFun (-f) = -UniformFun.toFun f
@[simp]
theorem UniformFun.toFun_inv {α : Type u_1} {β : Type u_2} [Inv β] (f : ) :
UniformFun.toFun f⁻¹ = (UniformFun.toFun f)⁻¹
@[simp]
theorem UniformFun.ofFun_neg {α : Type u_1} {β : Type u_2} [Neg β] (f : αβ) :
UniformFun.ofFun (-f) = -UniformFun.ofFun f
@[simp]
theorem UniformFun.ofFun_inv {α : Type u_1} {β : Type u_2} [Inv β] (f : αβ) :
UniformFun.ofFun f⁻¹ = (UniformFun.ofFun f)⁻¹
instance instNegUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Neg β] :
Neg (UniformOnFun α β 𝔖)
Equations
• instNegUniformOnFun = Pi.instNeg
instance instInvUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Inv β] :
Inv (UniformOnFun α β 𝔖)
Equations
• instInvUniformOnFun = Pi.instInv
@[simp]
theorem UniformOnFun.toFun_neg {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Neg β] (f : UniformOnFun α β 𝔖) :
(-f) = - f
@[simp]
theorem UniformOnFun.toFun_inv {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Inv β] (f : UniformOnFun α β 𝔖) :
f⁻¹ = ( f)⁻¹
@[simp]
theorem UniformOnFun.ofFun_neg {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Neg β] (f : αβ) :
(-f) = - f
@[simp]
theorem UniformOnFun.ofFun_inv {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Inv β] (f : αβ) :
f⁻¹ = ( f)⁻¹
instance instSubUniformFun {α : Type u_1} {β : Type u_2} [Sub β] :
Sub ()
Equations
• instSubUniformFun = Pi.instSub
instance instDivUniformFun {α : Type u_1} {β : Type u_2} [Div β] :
Div ()
Equations
• instDivUniformFun = Pi.instDiv
@[simp]
theorem UniformFun.toFun_sub {α : Type u_1} {β : Type u_2} [Sub β] (f : ) (g : ) :
UniformFun.toFun (f - g) = UniformFun.toFun f - UniformFun.toFun g
@[simp]
theorem UniformFun.toFun_div {α : Type u_1} {β : Type u_2} [Div β] (f : ) (g : ) :
UniformFun.toFun (f / g) = UniformFun.toFun f / UniformFun.toFun g
@[simp]
theorem UniformFun.ofFun_sub {α : Type u_1} {β : Type u_2} [Sub β] (f : αβ) (g : αβ) :
UniformFun.ofFun (f - g) = UniformFun.ofFun f - UniformFun.ofFun g
@[simp]
theorem UniformFun.ofFun_div {α : Type u_1} {β : Type u_2} [Div β] (f : αβ) (g : αβ) :
UniformFun.ofFun (f / g) = UniformFun.ofFun f / UniformFun.ofFun g
instance instSubUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Sub β] :
Sub (UniformOnFun α β 𝔖)
Equations
• instSubUniformOnFun = Pi.instSub
instance instDivUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Div β] :
Div (UniformOnFun α β 𝔖)
Equations
• instDivUniformOnFun = Pi.instDiv
@[simp]
theorem UniformOnFun.toFun_sub {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Sub β] (f : UniformOnFun α β 𝔖) (g : UniformOnFun α β 𝔖) :
(f - g) = f - g
@[simp]
theorem UniformOnFun.toFun_div {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Div β] (f : UniformOnFun α β 𝔖) (g : UniformOnFun α β 𝔖) :
(f / g) = f / g
@[simp]
theorem UniformOnFun.ofFun_sub {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Sub β] (f : αβ) (g : αβ) :
(f - g) = f - g
@[simp]
theorem UniformOnFun.ofFun_div {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Div β] (f : αβ) (g : αβ) :
(f / g) = f / g
instance instAddMonoidUniformFun {α : Type u_1} {β : Type u_2} [] :
Equations
instance instMonoidUniformFun {α : Type u_1} {β : Type u_2} [] :
Equations
• instMonoidUniformFun = Pi.monoid
instance instAddMonoidUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [] :
Equations
instance instMonoidUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [] :
Monoid (UniformOnFun α β 𝔖)
Equations
• instMonoidUniformOnFun = Pi.monoid
instance instAddCommMonoidUniformFun {α : Type u_1} {β : Type u_2} [] :
Equations
instance instCommMonoidUniformFun {α : Type u_1} {β : Type u_2} [] :
Equations
• instCommMonoidUniformFun = Pi.commMonoid
instance instAddCommMonoidUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [] :
Equations
instance instCommMonoidUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [] :
Equations
• instCommMonoidUniformOnFun = Pi.commMonoid
instance instAddGroupUniformFun {α : Type u_1} {β : Type u_2} [] :
Equations
instance instGroupUniformFun {α : Type u_1} {β : Type u_2} [] :
Equations
• instGroupUniformFun = Pi.group
instance instAddGroupUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [] :
Equations
instance instGroupUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [] :
Group (UniformOnFun α β 𝔖)
Equations
• instGroupUniformOnFun = Pi.group
instance instAddCommGroupUniformFun {α : Type u_1} {β : Type u_2} [] :
Equations
instance instCommGroupUniformFun {α : Type u_1} {β : Type u_2} [] :
Equations
• instCommGroupUniformFun = Pi.commGroup
instance instAddCommGroupUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [] :
Equations
instance instCommGroupUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [] :
CommGroup (UniformOnFun α β 𝔖)
Equations
• instCommGroupUniformOnFun = Pi.commGroup
instance instSMulUniformFun {α : Type u_1} {β : Type u_2} {M : Type u_5} [SMul M β] :
SMul M ()
Equations
• instSMulUniformFun = Pi.instSMul
@[simp]
theorem UniformFun.toFun_smul {α : Type u_1} {β : Type u_2} {M : Type u_5} [SMul M β] (c : M) (f : ) :
UniformFun.toFun (c f) = c UniformFun.toFun f
@[simp]
theorem UniformFun.ofFun_smul {α : Type u_1} {β : Type u_2} {M : Type u_5} [SMul M β] (c : M) (f : αβ) :
UniformFun.ofFun (c f) = c UniformFun.ofFun f
instance instSMulUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [SMul M β] :
SMul M (UniformOnFun α β 𝔖)
Equations
• instSMulUniformOnFun = Pi.instSMul
@[simp]
theorem UniformOnFun.toFun_smul {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [SMul M β] (c : M) (f : UniformOnFun α β 𝔖) :
(c f) = c f
@[simp]
theorem UniformOnFun.ofFun_smul {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [SMul M β] (c : M) (f : αβ) :
(c f) = c f
instance instIsScalarTowerUniformFun {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [SMul M N] [SMul M β] [SMul N β] [] :
Equations
• =
instance instIsScalarTowerUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} {N : Type u_6} [SMul M N] [SMul M β] [SMul N β] [] :
IsScalarTower M N (UniformOnFun α β 𝔖)
Equations
• =
instance instSMulCommClassUniformFun {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [SMul M β] [SMul N β] [] :
Equations
• =
instance instSMulCommClassUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} {N : Type u_6} [SMul M β] [SMul N β] [] :
SMulCommClass M N (UniformOnFun α β 𝔖)
Equations
• =
instance instMulActionUniformFun {α : Type u_1} {β : Type u_2} {M : Type u_5} [] [] :
Equations
• instMulActionUniformFun =
instance instMulActionUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [] [] :
MulAction M (UniformOnFun α β 𝔖)
Equations
• instMulActionUniformOnFun =
instance instDistribMulActionUniformFun {α : Type u_1} {β : Type u_2} {M : Type u_5} [] [] [] :
Equations
• instDistribMulActionUniformFun =
instance instDistribMulActionUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [] [] [] :
Equations
• instDistribMulActionUniformOnFun =
instance instModuleUniformFun {α : Type u_1} {β : Type u_2} {R : Type u_4} [] [] [Module R β] :
Module R ()
Equations
• instModuleUniformFun = Pi.module α (fun (a : α) => β) R
instance instModuleUniformOnFun {α : Type u_1} {β : Type u_2} {R : Type u_4} {𝔖 : Set (Set α)} [] [] [Module R β] :
Module R (UniformOnFun α β 𝔖)
Equations
• instModuleUniformOnFun = Pi.module α (fun (a : α) => β) R
instance instUniformAddGroupUniformFun {α : Type u_1} {G : Type u_2} [] [] [] :

If G is a uniform additive group, then α →ᵤ G is a uniform additive group as well.

Equations
• =
instance instUniformGroupUniformFun {α : Type u_1} {G : Type u_2} [] [] [] :

If G is a uniform group, then α →ᵤ G is a uniform group as well.

Equations
• =
theorem UniformFun.hasBasis_nhds_zero_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [] [] [] {p : ιProp} {b : ιSet G} (h : (nhds 0).HasBasis p b) :
(nhds 0).HasBasis p fun (i : ι) => {f : | ∀ (x : α), UniformFun.toFun f x b i}
theorem UniformFun.hasBasis_nhds_one_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [] [] [] {p : ιProp} {b : ιSet G} (h : (nhds 1).HasBasis p b) :
(nhds 1).HasBasis p fun (i : ι) => {f : | ∀ (x : α), UniformFun.toFun f x b i}
theorem UniformFun.hasBasis_nhds_zero {α : Type u_1} {G : Type u_2} [] [] [] :
(nhds 0).HasBasis (fun (V : Set G) => V nhds 0) fun (V : Set G) => {f : αG | ∀ (x : α), f x V}
theorem UniformFun.hasBasis_nhds_one {α : Type u_1} {G : Type u_2} [] [] [] :
(nhds 1).HasBasis (fun (V : Set G) => V nhds 1) fun (V : Set G) => {f : αG | ∀ (x : α), f x V}
instance instUniformAddGroupUniformOnFun {α : Type u_1} {G : Type u_2} [] {𝔖 : Set (Set α)} [] [] :

Let 𝔖 : Set (Set α). If G is a uniform additive group, then α →ᵤ[𝔖] G is a uniform additive group as well.

Equations
• =
instance instUniformGroupUniformOnFun {α : Type u_1} {G : Type u_2} [] {𝔖 : Set (Set α)} [] [] :

Let 𝔖 : Set (Set α). If G is a uniform group, then α →ᵤ[𝔖] G is a uniform group as well.

Equations
• =
theorem UniformOnFun.hasBasis_nhds_zero_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [] [] [] (𝔖 : Set (Set α)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (fun (x x_1 : Set α) => x x_1) 𝔖) {p : ιProp} {b : ιSet G} (h : (nhds 0).HasBasis p b) :
(nhds 0).HasBasis (fun (Si : Set α × ι) => Si.1 𝔖 p Si.2) fun (Si : Set α × ι) => {f : UniformOnFun α G 𝔖 | xSi.1, f x b Si.2}
theorem UniformOnFun.hasBasis_nhds_one_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [] [] [] (𝔖 : Set (Set α)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (fun (x x_1 : Set α) => x x_1) 𝔖) {p : ιProp} {b : ιSet G} (h : (nhds 1).HasBasis p b) :
(nhds 1).HasBasis (fun (Si : Set α × ι) => Si.1 𝔖 p Si.2) fun (Si : Set α × ι) => {f : UniformOnFun α G 𝔖 | xSi.1, f x b Si.2}
theorem UniformOnFun.hasBasis_nhds_zero {α : Type u_1} {G : Type u_2} [] [] [] (𝔖 : Set (Set α)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (fun (x x_1 : Set α) => x x_1) 𝔖) :
(nhds 0).HasBasis (fun (SV : Set α × Set G) => SV.1 𝔖 SV.2 nhds 0) fun (SV : Set α × Set G) => {f : UniformOnFun α G 𝔖 | xSV.1, f x SV.2}
theorem UniformOnFun.hasBasis_nhds_one {α : Type u_1} {G : Type u_2} [] [] [] (𝔖 : Set (Set α)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (fun (x x_1 : Set α) => x x_1) 𝔖) :
(nhds 1).HasBasis (fun (SV : Set α × Set G) => SV.1 𝔖 SV.2 nhds 1) fun (SV : Set α × Set G) => {f : UniformOnFun α G 𝔖 | xSV.1, f x SV.2}
instance UniformFun.uniformContinuousConstSMul (M : Type u_1) (α : Type u_2) (X : Type u_3) [SMul M X] [] :
Equations
• =
instance UniformFunOn.uniformContinuousConstSMul (M : Type u_1) (α : Type u_2) (X : Type u_3) [SMul M X] [] {𝔖 : Set (Set α)} :
Equations
• =
theorem UniformFun.continuousSMul_induced_of_range_bounded (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) (H : Type u_4) {hom : Type u_5} [] [] [Module 𝕜 H] [] [Module 𝕜 E] [] [] [] [] [FunLike hom H (αE)] [LinearMapClass hom 𝕜 H (αE)] (φ : hom) (hφ : Inducing (UniformFun.ofFun φ)) (h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))) :

Let E be a topological vector space over a normed field 𝕜, let α be any type. Let H be a submodule of α →ᵤ E such that the range of each f ∈ H is von Neumann bounded. Then H is a topological vector space over 𝕜, i.e., the pointwise scalar multiplication is continuous in both variables.

For convenience we require that H is a vector space over 𝕜 with a topology induced by UniformFun.ofFun ∘ φ, where φ : H →ₗ[𝕜] (α → E).

theorem UniformOnFun.continuousSMul_induced_of_image_bounded (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) (H : Type u_4) {hom : Type u_5} [] [] [Module 𝕜 H] [] [Module 𝕜 E] [] [] [] [] {𝔖 : Set (Set α)} [FunLike hom H (αE)] [LinearMapClass hom 𝕜 H (αE)] (φ : hom) (hφ : Inducing ( φ)) (h : ∀ (u : H), s𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)) :

Let E be a TVS, 𝔖 : Set (Set α) and H a submodule of α →ᵤ[𝔖] E. If the image of any S ∈ 𝔖 by any u ∈ H is bounded (in the sense of Bornology.IsVonNBounded), then H, equipped with the topology of 𝔖-convergence, is a TVS.

For convenience, we don't literally ask for H : Submodule (α →ᵤ[𝔖] E). Instead, we prove the result for any vector space H equipped with a linear inducing to α →ᵤ[𝔖] E, which is often easier to use. We also state the Submodule version as UniformOnFun.continuousSMul_submodule_of_image_bounded.

theorem UniformOnFun.continuousSMul_submodule_of_image_bounded (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) [] [] [Module 𝕜 E] [] [] [] {𝔖 : Set (Set α)} (H : Submodule 𝕜 (UniformOnFun α E 𝔖)) (h : uH, s𝔖, Bornology.IsVonNBounded 𝕜 (u '' s)) :

Let E be a TVS, 𝔖 : Set (Set α) and H a submodule of α →ᵤ[𝔖] E. If the image of any S ∈ 𝔖 by any u ∈ H is bounded (in the sense of Bornology.IsVonNBounded), then H, equipped with the topology of 𝔖-convergence, is a TVS.

If you have a hard time using this lemma, try the one above instead.