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.

Implementation notes #

Like in Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean, 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 instOneUniformFun {α : Type u_1} {β : Type u_2} [One β] :

One (UniformFun α β)

Equations

instance instZeroUniformFun {α : Type u_1} {β : Type u_2} [Zero β] :

Zero (UniformFun α β)

Equations

@[simp]

theorem UniformFun.toFun_one {α : Type u_1} {β : Type u_2} [One β] :

@[simp]

theorem UniformFun.toFun_zero {α : Type u_1} {β : Type u_2} [Zero β] :

@[simp]

theorem UniformFun.ofFun_one {α : Type u_1} {β : Type u_2} [One β] :

@[simp]

theorem UniformFun.ofFun_zero {α : Type u_1} {β : Type u_2} [Zero β] :

instance instOneUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [One β] :

One (UniformOnFun α β 𝔖)

Equations

instance instZeroUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Zero β] :

Zero (UniformOnFun α β 𝔖)

Equations

@[simp]

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

(toFun 𝔖) 1 = 1

@[simp]

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

(toFun 𝔖) 0 = 0

@[simp]

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

(ofFun 𝔖) 1 = 1

@[simp]

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

(ofFun 𝔖) 0 = 0

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

Mul (UniformFun α β)

Equations

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

Add (UniformFun α β)

Equations

@[simp]

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

toFun (f * g) = toFun f * toFun g

@[simp]

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

toFun (f + g) = toFun f + toFun g

@[simp]

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

ofFun (f * g) = ofFun f * ofFun g

@[simp]

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

ofFun (f + g) = ofFun f + ofFun g

instance instMulUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Mul β] :

Mul (UniformOnFun α β 𝔖)

Equations

instance instAddUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Add β] :

Add (UniformOnFun α β 𝔖)

Equations

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

Inv (UniformFun α β)

Equations

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

Neg (UniformFun α β)

Equations

@[simp]

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

toFun f⁻¹ = (toFun f)⁻¹

@[simp]

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

toFun (-f) = -toFun f

@[simp]

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

ofFun f⁻¹ = (ofFun f)⁻¹

@[simp]

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

ofFun (-f) = -ofFun f

instance instInvUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Inv β] :

Inv (UniformOnFun α β 𝔖)

Equations

instance instNegUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Neg β] :

Neg (UniformOnFun α β 𝔖)

Equations

@[simp]

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

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

@[simp]

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

(toFun 𝔖) (-f) = -(toFun 𝔖) f

@[simp]

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

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

@[simp]

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

(ofFun 𝔖) (-f) = -(ofFun 𝔖) f

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

Div (UniformFun α β)

Equations

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

Sub (UniformFun α β)

Equations

@[simp]

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

toFun (f / g) = toFun f / toFun g

@[simp]

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

toFun (f - g) = toFun f - toFun g

@[simp]

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

ofFun (f / g) = ofFun f / ofFun g

@[simp]

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

ofFun (f - g) = ofFun f - ofFun g

instance instDivUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Div β] :

Div (UniformOnFun α β 𝔖)

Equations

instance instSubUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Sub β] :

Sub (UniformOnFun α β 𝔖)

Equations

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

Monoid (UniformFun α β)

Equations

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

AddMonoid (UniformFun α β)

Equations

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

Monoid (UniformOnFun α β 𝔖)

Equations

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

AddMonoid (UniformOnFun α β 𝔖)

Equations

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

CommMonoid (UniformFun α β)

Equations

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

AddCommMonoid (UniformFun α β)

Equations

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

CommMonoid (UniformOnFun α β 𝔖)

Equations

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

AddCommMonoid (UniformOnFun α β 𝔖)

Equations

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

Group (UniformFun α β)

Equations

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

AddGroup (UniformFun α β)

Equations

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

Group (UniformOnFun α β 𝔖)

Equations

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

AddGroup (UniformOnFun α β 𝔖)

Equations

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

CommGroup (UniformFun α β)

Equations

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

AddCommGroup (UniformFun α β)

Equations

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

CommGroup (UniformOnFun α β 𝔖)

Equations

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

AddCommGroup (UniformOnFun α β 𝔖)

Equations

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

SMul M (UniformFun α β)

Equations

@[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 • toFun f

@[simp]

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

ofFun (c • f) = c • ofFun f

instance instSMulUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [SMul M β] :

SMul M (UniformOnFun α β 𝔖)

Equations

@[simp]

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

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

@[simp]

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

(ofFun 𝔖) (c • f) = c • (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 α β)

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

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

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

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

MulAction M (UniformFun α β)

Equations

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

MulAction M (UniformOnFun α β 𝔖)

Equations

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

DistribMulAction M (UniformFun α β)

Equations

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

DistribMulAction M (UniformOnFun α β 𝔖)

Equations

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

Module R (UniformFun α β)

Equations

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

Module R (UniformOnFun α β 𝔖)

Equations

instance instIsUniformGroupUniformFun {α : Type u_1} {G : Type u_2} [Group G] [UniformSpace G] [IsUniformGroup G] :

IsUniformGroup (UniformFun α G)

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

instance instIsUniformAddGroupUniformFun {α : Type u_1} {G : Type u_2} [AddGroup G] [UniformSpace G] [IsUniformAddGroup G] :

IsUniformAddGroup (UniformFun α G)

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

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

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

theorem UniformFun.hasBasis_nhds_zero_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [AddGroup G] [UniformSpace G] [IsUniformAddGroup G] {p : ι → Prop} {b : ι → Set G} (h : (nhds 0).HasBasis p b) :

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

theorem UniformFun.hasBasis_nhds_one {α : Type u_1} {G : Type u_2} [Group G] [UniformSpace G] [IsUniformGroup G] :

(nhds 1).HasBasis (fun (V : Set G) => V ∈ nhds 1) fun (V : Set G) => {f : α → G | ∀ (x : α), f x ∈ V}

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

(nhds 0).HasBasis (fun (V : Set G) => V ∈ nhds 0) fun (V : Set G) => {f : α → G | ∀ (x : α), f x ∈ V}

instance instIsUniformGroupUniformOnFun {α : Type u_1} {G : Type u_2} [Group G] {𝔖 : Set (Set α)} [UniformSpace G] [IsUniformGroup G] :

IsUniformGroup (UniformOnFun α G 𝔖)

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

instance instIsUniformAddGroupUniformOnFun {α : Type u_1} {G : Type u_2} [AddGroup G] {𝔖 : Set (Set α)} [UniformSpace G] [IsUniformAddGroup G] :

IsUniformAddGroup (UniformOnFun α G 𝔖)

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

theorem UniformOnFun.hasBasis_nhds_one_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [Group G] [UniformSpace G] [IsUniformGroup G] (𝔖 : Set (Set α)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) 𝔖) {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, (toFun 𝔖) f x ∈ b Si.2}

theorem UniformOnFun.hasBasis_nhds_zero_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [AddGroup G] [UniformSpace G] [IsUniformAddGroup G] (𝔖 : Set (Set α)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) 𝔖) {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, (toFun 𝔖) f x ∈ b Si.2}

theorem UniformOnFun.hasBasis_nhds_one {α : Type u_1} {G : Type u_2} [Group G] [UniformSpace G] [IsUniformGroup G] (𝔖 : Set (Set α)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) 𝔖) :

(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}

theorem UniformOnFun.hasBasis_nhds_zero {α : Type u_1} {G : Type u_2} [AddGroup G] [UniformSpace G] [IsUniformAddGroup G] (𝔖 : Set (Set α)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) 𝔖) :

(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}

@[simp]

theorem UniformOnFun.ofFun_prod {α : Type u_1} {ι : Type u_3} {𝔖 : Set (Set α)} {β : Type u_4} [CommMonoid β] {f : ι → α → β} (I : Finset ι) :

(ofFun 𝔖) (∏ i ∈ I, f i) = ∏ i ∈ I, (ofFun 𝔖) (f i)

@[simp]

theorem UniformOnFun.ofFun_sum {α : Type u_1} {ι : Type u_3} {𝔖 : Set (Set α)} {β : Type u_4} [AddCommMonoid β] {f : ι → α → β} (I : Finset ι) :

(ofFun 𝔖) (∑ i ∈ I, f i) = ∑ i ∈ I, (ofFun 𝔖) (f i)

@[simp]

theorem UniformOnFun.toFun_prod {α : Type u_1} {ι : Type u_3} {𝔖 : Set (Set α)} {β : Type u_4} [CommMonoid β] {f : ι → α → β} (I : Finset ι) :

(toFun 𝔖) (∏ i ∈ I, f i) = ∏ i ∈ I, (toFun 𝔖) (f i)

@[simp]

theorem UniformOnFun.toFun_sum {α : Type u_1} {ι : Type u_3} {𝔖 : Set (Set α)} {β : Type u_4} [AddCommMonoid β] {f : ι → α → β} (I : Finset ι) :

(toFun 𝔖) (∑ i ∈ I, f i) = ∑ i ∈ I, (toFun 𝔖) (f i)

@[simp]

theorem UniformFun.ofFun_prod {α : Type u_1} {ι : Type u_3} {β : Type u_4} [CommMonoid β] {f : ι → α → β} (I : Finset ι) :

ofFun (∏ i ∈ I, f i) = ∏ i ∈ I, ofFun (f i)

@[simp]

theorem UniformFun.ofFun_sum {α : Type u_1} {ι : Type u_3} {β : Type u_4} [AddCommMonoid β] {f : ι → α → β} (I : Finset ι) :

ofFun (∑ i ∈ I, f i) = ∑ i ∈ I, ofFun (f i)

@[simp]

theorem UniformFun.toFun_prod {α : Type u_1} {ι : Type u_3} {β : Type u_4} [CommMonoid β] {f : ι → α → β} (I : Finset ι) :

toFun (∏ i ∈ I, f i) = ∏ i ∈ I, toFun (f i)

@[simp]

theorem UniformFun.toFun_sum {α : Type u_1} {ι : Type u_3} {β : Type u_4} [AddCommMonoid β] {f : ι → α → β} (I : Finset ι) :

toFun (∑ i ∈ I, f i) = ∑ i ∈ I, toFun (f i)

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)

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 𝔖)