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 instIsScalarTowerUniformFunInstSMulUniformFunInstSMulUniformFun {α : 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

• (_ : IsScalarTower M N (UniformFun α β)) = (_ : IsScalarTower M N (α → β))

instance instIsScalarTowerUniformOnFunInstSMulUniformOnFunInstSMulUniformOnFun {α : 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

• (_ : IsScalarTower M N (UniformOnFun α β 𝔖)) = (_ : IsScalarTower M N (α → β))

instance instSMulCommClassUniformFunInstSMulUniformFunInstSMulUniformFun {α : 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

• (_ : SMulCommClass M N (UniformFun α β)) = (_ : SMulCommClass M N (α → β))

instance instSMulCommClassUniformOnFunInstSMulUniformOnFunInstSMulUniformOnFun {α : 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

• (_ : SMulCommClass M N (UniformOnFun α β 𝔖)) = (_ : SMulCommClass M N (α → β))

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 instDistribMulActionUniformFunInstAddMonoidUniformFun {α : Type u_1} {β : Type u_2} {M : Type u_5} [Monoid M] [AddMonoid β] [DistribMulAction M β] : DistribMulAction M (UniformFun α β)

Equations

• instDistribMulActionUniformFunInstAddMonoidUniformFun = Pi.distribMulAction M

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

Equations

• instDistribMulActionUniformOnFunInstAddMonoidUniformOnFun = Pi.distribMulAction M

instance instModuleUniformFunInstAddCommMonoidUniformFun {α : Type u_1} {β : Type u_2} {R : Type u_4} [Semiring R] [AddCommMonoid β] [Module R β] : Module R (UniformFun α β)

Equations

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

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

Equations

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

instance instUniformAddGroupUniformFunUniformSpaceInstAddGroupUniformFun {α : 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

• (_ : UniformAddGroup (UniformFun α G)) = (_ : UniformAddGroup (UniformFun α G))

instance instUniformGroupUniformFunUniformSpaceInstGroupUniformFun {α : 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

• (_ : UniformGroup (UniformFun α G)) = (_ : UniformGroup (UniformFun α G))

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 : Filter.HasBasis (nhds 0) p b) : Filter.HasBasis (nhds 0) 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 : Filter.HasBasis (nhds 1) p b) : Filter.HasBasis (nhds 1) 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] : Filter.HasBasis (nhds 0) (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] : Filter.HasBasis (nhds 1) (fun (V : Set G) => V ∈ nhds 1) fun (V : Set G) => {f : α → G | ∀ (x : α), f x ∈ V}

instance instUniformAddGroupUniformOnFunUniformSpaceInstAddGroupUniformOnFun {α : 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

• (_ : UniformAddGroup (UniformOnFun α G 𝔖)) = (_ : UniformAddGroup (UniformOnFun α G 𝔖))

instance instUniformGroupUniformOnFunUniformSpaceInstGroupUniformOnFun {α : 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

• (_ : UniformGroup (UniformOnFun α G 𝔖)) = (_ : UniformGroup (UniformOnFun α G 𝔖))

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𝔖₁ : Set.Nonempty 𝔖) (h𝔖₂ : DirectedOn (fun (x x_1 : Set α) => x ⊆ x_1) 𝔖) {p : ι → Prop} {b : ι → Set G} (h : Filter.HasBasis (nhds 0) p b) : Filter.HasBasis (nhds 0) (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𝔖₁ : Set.Nonempty 𝔖) (h𝔖₂ : DirectedOn (fun (x x_1 : Set α) => x ⊆ x_1) 𝔖) {p : ι → Prop} {b : ι → Set G} (h : Filter.HasBasis (nhds 1) p b) : Filter.HasBasis (nhds 1) (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𝔖₁ : Set.Nonempty 𝔖) (h𝔖₂ : DirectedOn (fun (x x_1 : Set α) => x ⊆ x_1) 𝔖) : Filter.HasBasis (nhds 0) (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𝔖₁ : Set.Nonempty 𝔖) (h𝔖₂ : DirectedOn (fun (x x_1 : Set α) => x ⊆ x_1) 𝔖) : Filter.HasBasis (nhds 1) (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

• (_ : UniformContinuousConstSMul M (UniformFun α X)) = (_ : UniformContinuousConstSMul M (UniformFun α X))

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

• (_ : UniformContinuousConstSMul M (UniformOnFun α X 𝔖)) = (_ : UniformContinuousConstSMul M (UniformOnFun α X 𝔖))

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.