Documentation

Mathlib.Topology.Algebra.UniformConvergence

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 (UniformFun α β)

Equations

instZeroUniformFun = Pi.instZero

instance instOneUniformFun {α : Type u_1} {β : Type u_2} [One β] :

One (UniformFun α β)

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 β] :

(UniformOnFun.toFun 𝔖) 0 = 0

@[simp]

theorem UniformOnFun.toFun_one {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [One β] :

(UniformOnFun.toFun 𝔖) 1 = 1

@[simp]

theorem UniformOnFun.zero_apply {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Zero β] :

(UniformOnFun.ofFun 𝔖) 0 = 0

@[simp]

theorem UniformOnFun.one_apply {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [One β] :

(UniformOnFun.ofFun 𝔖) 1 = 1

instance instAddUniformFun {α : Type u_1} {β : Type u_2} [Add β] :

Add (UniformFun α β)

Equations

instAddUniformFun = Pi.instAdd

instance instMulUniformFun {α : Type u_1} {β : Type u_2} [Mul β] :

Mul (UniformFun α β)

Equations

instMulUniformFun = Pi.instMul

@[simp]

theorem UniformFun.toFun_add {α : Type u_1} {β : Type u_2} [Add β] (f : UniformFun α β) (g : UniformFun α β) :

UniformFun.toFun (f + g) = UniformFun.toFun f + UniformFun.toFun g

@[simp]

theorem UniformFun.toFun_mul {α : Type u_1} {β : Type u_2} [Mul β] (f : UniformFun α β) (g : UniformFun α β) :

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 β] :

Add (UniformOnFun α β 𝔖)

Equations

instAddUniformOnFun = Pi.instAdd

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 α β 𝔖) :

(UniformOnFun.toFun 𝔖) (f + g) = (UniformOnFun.toFun 𝔖) f + (UniformOnFun.toFun 𝔖) g

@[simp]

theorem UniformOnFun.toFun_mul {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Mul β] (f : UniformOnFun α β 𝔖) (g : UniformOnFun α β 𝔖) :

(UniformOnFun.toFun 𝔖) (f * g) = (UniformOnFun.toFun 𝔖) f * (UniformOnFun.toFun 𝔖) g

@[simp]

theorem UniformOnFun.ofFun_add {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Add β] (f : α → β) (g : α → β) :

(UniformOnFun.ofFun 𝔖) (f + g) = (UniformOnFun.ofFun 𝔖) f + (UniformOnFun.ofFun 𝔖) g

@[simp]

theorem UniformOnFun.ofFun_mul {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Mul β] (f : α → β) (g : α → β) :

(UniformOnFun.ofFun 𝔖) (f * g) = (UniformOnFun.ofFun 𝔖) f * (UniformOnFun.ofFun 𝔖) g

instance instNegUniformFun {α : Type u_1} {β : Type u_2} [Neg β] :

Neg (UniformFun α β)

Equations

instNegUniformFun = Pi.instNeg

instance instInvUniformFun {α : Type u_1} {β : Type u_2} [Inv β] :

Inv (UniformFun α β)

Equations

instInvUniformFun = Pi.instInv

@[simp]

theorem UniformFun.toFun_neg {α : Type u_1} {β : Type u_2} [Neg β] (f : UniformFun α β) :

UniformFun.toFun (-f) = -UniformFun.toFun f

@[simp]

theorem UniformFun.toFun_inv {α : Type u_1} {β : Type u_2} [Inv β] (f : UniformFun α β) :

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 α β 𝔖) :

(UniformOnFun.toFun 𝔖) (-f) = -(UniformOnFun.toFun 𝔖) f

@[simp]

theorem UniformOnFun.toFun_inv {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Inv β] (f : UniformOnFun α β 𝔖) :

(UniformOnFun.toFun 𝔖) f⁻¹ = ((UniformOnFun.toFun 𝔖) f)⁻¹

@[simp]

theorem UniformOnFun.ofFun_neg {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Neg β] (f : α → β) :

(UniformOnFun.ofFun 𝔖) (-f) = -(UniformOnFun.ofFun 𝔖) f

@[simp]

theorem UniformOnFun.ofFun_inv {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Inv β] (f : α → β) :

(UniformOnFun.ofFun 𝔖) f⁻¹ = ((UniformOnFun.ofFun 𝔖) f)⁻¹

instance instSubUniformFun {α : Type u_1} {β : Type u_2} [Sub β] :

Sub (UniformFun α β)

Equations

instSubUniformFun = Pi.instSub

instance instDivUniformFun {α : Type u_1} {β : Type u_2} [Div β] :

Div (UniformFun α β)

Equations

instDivUniformFun = Pi.instDiv

@[simp]

theorem UniformFun.toFun_sub {α : Type u_1} {β : Type u_2} [Sub β] (f : UniformFun α β) (g : UniformFun α β) :

UniformFun.toFun (f - g) = UniformFun.toFun f - UniformFun.toFun g

@[simp]

theorem UniformFun.toFun_div {α : Type u_1} {β : Type u_2} [Div β] (f : UniformFun α β) (g : UniformFun α β) :

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 α β 𝔖) :

(UniformOnFun.toFun 𝔖) (f - g) = (UniformOnFun.toFun 𝔖) f - (UniformOnFun.toFun 𝔖) g

@[simp]

theorem UniformOnFun.toFun_div {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Div β] (f : UniformOnFun α β 𝔖) (g : UniformOnFun α β 𝔖) :

(UniformOnFun.toFun 𝔖) (f / g) = (UniformOnFun.toFun 𝔖) f / (UniformOnFun.toFun 𝔖) g

@[simp]

theorem UniformOnFun.ofFun_sub {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Sub β] (f : α → β) (g : α → β) :

(UniformOnFun.ofFun 𝔖) (f - g) = (UniformOnFun.ofFun 𝔖) f - (UniformOnFun.ofFun 𝔖) g

@[simp]

theorem UniformOnFun.ofFun_div {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Div β] (f : α → β) (g : α → β) :

(UniformOnFun.ofFun 𝔖) (f / g) = (UniformOnFun.ofFun 𝔖) f / (UniformOnFun.ofFun 𝔖) g

instance instAddMonoidUniformFun {α : Type u_1} {β : Type u_2} [AddMonoid β] :

AddMonoid (UniformFun α β)

Equations

instAddMonoidUniformFun = Pi.addMonoid

instance instMonoidUniformFun {α : Type u_1} {β : Type u_2} [Monoid β] :

Monoid (UniformFun α β)

Equations

instMonoidUniformFun = Pi.monoid

instance instAddMonoidUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddMonoid β] :

AddMonoid (UniformOnFun α β 𝔖)

Equations

instAddMonoidUniformOnFun = Pi.addMonoid

instance instMonoidUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Monoid β] :

Monoid (UniformOnFun α β 𝔖)

Equations

instMonoidUniformOnFun = Pi.monoid

instance instAddCommMonoidUniformFun {α : Type u_1} {β : Type u_2} [AddCommMonoid β] :

AddCommMonoid (UniformFun α β)

Equations

instAddCommMonoidUniformFun = Pi.addCommMonoid

instance instCommMonoidUniformFun {α : Type u_1} {β : Type u_2} [CommMonoid β] :

CommMonoid (UniformFun α β)

Equations

instCommMonoidUniformFun = Pi.commMonoid

instance instAddCommMonoidUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddCommMonoid β] :

AddCommMonoid (UniformOnFun α β 𝔖)

Equations

instAddCommMonoidUniformOnFun = Pi.addCommMonoid

instance instCommMonoidUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [CommMonoid β] :

CommMonoid (UniformOnFun α β 𝔖)

Equations

instCommMonoidUniformOnFun = Pi.commMonoid

instance instAddGroupUniformFun {α : Type u_1} {β : Type u_2} [AddGroup β] :

AddGroup (UniformFun α β)

Equations

instAddGroupUniformFun = Pi.addGroup

instance instGroupUniformFun {α : Type u_1} {β : Type u_2} [Group β] :

Group (UniformFun α β)

Equations

instGroupUniformFun = Pi.group

instance instAddGroupUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddGroup β] :

AddGroup (UniformOnFun α β 𝔖)

Equations

instAddGroupUniformOnFun = Pi.addGroup

instance instGroupUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Group β] :

Group (UniformOnFun α β 𝔖)

Equations

instGroupUniformOnFun = Pi.group

instance instAddCommGroupUniformFun {α : Type u_1} {β : Type u_2} [AddCommGroup β] :

AddCommGroup (UniformFun α β)

Equations

instAddCommGroupUniformFun = Pi.addCommGroup

instance instCommGroupUniformFun {α : Type u_1} {β : Type u_2} [CommGroup β] :

CommGroup (UniformFun α β)

Equations

instCommGroupUniformFun = Pi.commGroup

instance instAddCommGroupUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddCommGroup β] :

AddCommGroup (UniformOnFun α β 𝔖)

Equations

instAddCommGroupUniformOnFun = Pi.addCommGroup

instance instCommGroupUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [CommGroup β] :

CommGroup (UniformOnFun α β 𝔖)

Equations

instCommGroupUniformOnFun = Pi.commGroup

instance instSMulUniformFun {α : Type u_1} {β : Type u_2} {M : Type u_5} [SMul M β] :

SMul M (UniformFun α β)

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 α β) :

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 α β 𝔖) :

(UniformOnFun.toFun 𝔖) (c • f) = c • (UniformOnFun.toFun 𝔖) f

@[simp]

theorem UniformOnFun.ofFun_smul {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [SMul M β] (c : M) (f : α → β) :

(UniformOnFun.ofFun 𝔖) (c • f) = c • (UniformOnFun.ofFun 𝔖) f

instance instIsScalarTowerUniformFun {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [SMul M N] [SMul M β] [SMul N β] [IsScalarTower M N β] :

IsScalarTower M N (UniformFun α β)

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 β] :

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 β] [SMulCommClass M N β] :

SMulCommClass M N (UniformFun α β)

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 β] :

SMulCommClass M N (UniformOnFun α β 𝔖)

Equations

⋯ = ⋯

instance instMulActionUniformFun {α : Type u_1} {β : Type u_2} {M : Type u_5} [Monoid M] [MulAction M β] :

MulAction M (UniformFun α β)

Equations

instMulActionUniformFun = Pi.mulAction M

instance instMulActionUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [Monoid M] [MulAction M β] :

MulAction M (UniformOnFun α β 𝔖)

Equations

instMulActionUniformOnFun = Pi.mulAction M

instance instDistribMulActionUniformFun {α : Type u_1} {β : Type u_2} {M : Type u_5} [Monoid M] [AddMonoid β] [DistribMulAction M β] :

DistribMulAction M (UniformFun α β)

Equations

instDistribMulActionUniformFun = Pi.distribMulAction M

instance instDistribMulActionUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [Monoid M] [AddMonoid β] [DistribMulAction M β] :

DistribMulAction M (UniformOnFun α β 𝔖)

Equations

instDistribMulActionUniformOnFun = Pi.distribMulAction M

instance instModuleUniformFun {α : Type u_1} {β : Type u_2} {R : Type u_4} [Semiring R] [AddCommMonoid β] [Module R β] :

Module R (UniformFun α β)

Equations

instModuleUniformFun = Pi.module α (fun (a : α) => β) R

instance instModuleUniformOnFun {α : Type u_1} {β : Type u_2} {R : Type u_4} {𝔖 : Set (Set α)} [Semiring R] [AddCommMonoid β] [Module R β] :

Module R (UniformOnFun α β 𝔖)

Equations

instModuleUniformOnFun = Pi.module α (fun (a : α) => β) R

instance instUniformAddGroupUniformFun {α : Type u_1} {G : Type u_2} [AddGroup G] [UniformSpace G] [UniformAddGroup G] :

UniformAddGroup (UniformFun α G)

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} [Group G] [UniformSpace G] [UniformGroup G] :

UniformGroup (UniformFun α G)

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} [AddGroup G] [UniformSpace G] [UniformAddGroup G] {p : ι → Prop} {b : ι → Set G} (h : (nhds 0).HasBasis p b) :

(nhds 0).HasBasis p fun (i : ι) => {f : UniformFun α G | ∀ (x : α), UniformFun.toFun f x ∈ b i}

theorem UniformFun.hasBasis_nhds_one_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [Group G] [UniformSpace G] [UniformGroup G] {p : ι → Prop} {b : ι → Set G} (h : (nhds 1).HasBasis p b) :

(nhds 1).HasBasis p fun (i : ι) => {f : UniformFun α G | ∀ (x : α), UniformFun.toFun f x ∈ b i}

theorem UniformFun.hasBasis_nhds_zero {α : Type u_1} {G : Type u_2} [AddGroup G] [UniformSpace G] [UniformAddGroup G] :

(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} [Group G] [UniformSpace G] [UniformGroup G] :

(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} [AddGroup G] {𝔖 : Set (Set α)} [UniformSpace G] [UniformAddGroup G] :

UniformAddGroup (UniformOnFun α G 𝔖)

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} [Group G] {𝔖 : Set (Set α)} [UniformSpace G] [UniformGroup G] :

UniformGroup (UniformOnFun α G 𝔖)

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} [AddGroup G] [UniformSpace G] [UniformAddGroup G] (𝔖 : 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 𝔖 | ∀ x ∈ Si.1, (UniformOnFun.toFun 𝔖) f x ∈ b Si.2}

theorem UniformOnFun.hasBasis_nhds_one_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [Group G] [UniformSpace G] [UniformGroup G] (𝔖 : 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 𝔖 | ∀ x ∈ Si.1, (UniformOnFun.toFun 𝔖) f x ∈ b Si.2}

theorem UniformOnFun.hasBasis_nhds_zero {α : Type u_1} {G : Type u_2} [AddGroup G] [UniformSpace G] [UniformAddGroup G] (𝔖 : 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 𝔖 | ∀ x ∈ SV.1, f x ∈ SV.2}

theorem UniformOnFun.hasBasis_nhds_one {α : Type u_1} {G : Type u_2} [Group G] [UniformSpace G] [UniformGroup G] (𝔖 : 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 𝔖 | ∀ x ∈ SV.1, f x ∈ SV.2}

instance UniformFun.uniformContinuousConstSMul (M : Type u_1) (α : Type u_2) (X : Type u_3) [SMul M X] [UniformSpace X] [UniformContinuousConstSMul M X] :

UniformContinuousConstSMul M (UniformFun α X)

Equations

⋯ = ⋯

instance UniformFunOn.uniformContinuousConstSMul (M : Type u_1) (α : Type u_2) (X : Type u_3) [SMul M X] [UniformSpace X] [UniformContinuousConstSMul M X] {𝔖 : Set (Set α)} :

UniformContinuousConstSMul M (UniformOnFun α X 𝔖)

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} [NormedField 𝕜] [AddCommGroup H] [Module 𝕜 H] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace H] [UniformSpace E] [UniformAddGroup E] [ContinuousSMul 𝕜 E] [FunLike hom H (α → E)] [LinearMapClass hom 𝕜 H (α → E)] (φ : hom) (hφ : Inducing (⇑UniformFun.ofFun ∘ ⇑φ)) (h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))) :

ContinuousSMul 𝕜 H

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} [NormedField 𝕜] [AddCommGroup H] [Module 𝕜 H] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace H] [UniformSpace E] [UniformAddGroup E] [ContinuousSMul 𝕜 E] {𝔖 : Set (Set α)} [FunLike hom H (α → E)] [LinearMapClass hom 𝕜 H (α → E)] (φ : hom) (hφ : Inducing (⇑(UniformOnFun.ofFun 𝔖) ∘ ⇑φ)) (h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)) :

ContinuousSMul 𝕜 H

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) [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [UniformSpace E] [UniformAddGroup E] [ContinuousSMul 𝕜 E] {𝔖 : Set (Set α)} (H : Submodule 𝕜 (UniformOnFun α E 𝔖)) (h : ∀ u ∈ H, ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (u '' s)) :

ContinuousSMul 𝕜 ↥H

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.