# 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

source
instance instOneUniformFun {α : Type u_1} {β : Type u_2} [One β] :
One (UniformFun α β)
Equations

- instOneUniformFun = Pi.instOne

source
instance instZeroUniformFun {α : Type u_1} {β : Type u_2} [Zero β] :
Zero (UniformFun α β)
Equations

- instZeroUniformFun = Pi.instZero

source
@[simp]
theorem UniformFun.toFun_one {α : Type u_1} {β : Type u_2} [One β] :
toFun 1 = 1
source
@[simp]
theorem UniformFun.toFun_zero {α : Type u_1} {β : Type u_2} [Zero β] :
toFun 0 = 0
source
@[simp]
theorem UniformFun.ofFun_one {α : Type u_1} {β : Type u_2} [One β] :
ofFun 1 = 1
source
@[simp]
theorem UniformFun.ofFun_zero {α : Type u_1} {β : Type u_2} [Zero β] :
ofFun 0 = 0
source
instance instOneUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [One β] :
One (UniformOnFun α β 𝔖)
Equations

- instOneUniformOnFun = Pi.instOne

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

- instZeroUniformOnFun = Pi.instZero

source
@[simp]
theorem UniformOnFun.toFun_one {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [One β] :
(toFun 𝔖) 1 = 1
source
@[simp]
theorem UniformOnFun.toFun_zero {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Zero β] :
(toFun 𝔖) 0 = 0
source
@[simp]
theorem UniformOnFun.one_apply {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [One β] :
(ofFun 𝔖) 1 = 1
source
@[simp]
theorem UniformOnFun.zero_apply {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Zero β] :
(ofFun 𝔖) 0 = 0
source
instance instMulUniformFun {α : Type u_1} {β : Type u_2} [Mul β] :
Mul (UniformFun α β)
Equations

- instMulUniformFun = Pi.instMul

source
instance instAddUniformFun {α : Type u_1} {β : Type u_2} [Add β] :
Add (UniformFun α β)
Equations

- instAddUniformFun = Pi.instAdd

source
@[simp]
theorem UniformFun.toFun_mul {α : Type u_1} {β : Type u_2} [Mul β] (f g : UniformFun α β) :
toFun (f * g) = toFun f * toFun g
source
@[simp]
theorem UniformFun.toFun_add {α : Type u_1} {β : Type u_2} [Add β] (f g : UniformFun α β) :
toFun (f + g) = toFun f + toFun g
source
@[simp]
theorem UniformFun.ofFun_mul {α : Type u_1} {β : Type u_2} [Mul β] (f g : α → β) :
ofFun (f * g) = ofFun f * ofFun g
source
@[simp]
theorem UniformFun.ofFun_add {α : Type u_1} {β : Type u_2} [Add β] (f g : α → β) :
ofFun (f + g) = ofFun f + ofFun g
source
instance instMulUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Mul β] :
Mul (UniformOnFun α β 𝔖)
Equations

- instMulUniformOnFun = Pi.instMul

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

- instAddUniformOnFun = Pi.instAdd

source
@[simp]
theorem UniformOnFun.toFun_mul {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Mul β] (f g : UniformOnFun α β 𝔖) :
(toFun 𝔖) (f * g) = (toFun 𝔖) f * (toFun 𝔖) g
source
@[simp]
theorem UniformOnFun.toFun_add {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Add β] (f g : UniformOnFun α β 𝔖) :
(toFun 𝔖) (f + g) = (toFun 𝔖) f + (toFun 𝔖) g
source
@[simp]
theorem UniformOnFun.ofFun_mul {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Mul β] (f g : α → β) :
(ofFun 𝔖) (f * g) = (ofFun 𝔖) f * (ofFun 𝔖) g
source
@[simp]
theorem UniformOnFun.ofFun_add {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Add β] (f g : α → β) :
(ofFun 𝔖) (f + g) = (ofFun 𝔖) f + (ofFun 𝔖) g
source
instance instInvUniformFun {α : Type u_1} {β : Type u_2} [Inv β] :
Inv (UniformFun α β)
Equations

- instInvUniformFun = Pi.instInv

source
instance instNegUniformFun {α : Type u_1} {β : Type u_2} [Neg β] :
Neg (UniformFun α β)
Equations

- instNegUniformFun = Pi.instNeg

source
@[simp]
theorem UniformFun.toFun_inv {α : Type u_1} {β : Type u_2} [Inv β] (f : UniformFun α β) :
toFun f⁻¹ = (toFun f)⁻¹
source
@[simp]
theorem UniformFun.toFun_neg {α : Type u_1} {β : Type u_2} [Neg β] (f : UniformFun α β) :
toFun (-f) = -toFun f
source
@[simp]
theorem UniformFun.ofFun_inv {α : Type u_1} {β : Type u_2} [Inv β] (f : α → β) :
ofFun f⁻¹ = (ofFun f)⁻¹
source
@[simp]
theorem UniformFun.ofFun_neg {α : Type u_1} {β : Type u_2} [Neg β] (f : α → β) :
ofFun (-f) = -ofFun f
source
instance instInvUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Inv β] :
Inv (UniformOnFun α β 𝔖)
Equations

- instInvUniformOnFun = Pi.instInv

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

- instNegUniformOnFun = Pi.instNeg

source
@[simp]
theorem UniformOnFun.toFun_inv {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Inv β] (f : UniformOnFun α β 𝔖) :
(toFun 𝔖) f⁻¹ = ((toFun 𝔖) f)⁻¹
source
@[simp]
theorem UniformOnFun.toFun_neg {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Neg β] (f : UniformOnFun α β 𝔖) :
(toFun 𝔖) (-f) = -(toFun 𝔖) f
source
@[simp]
theorem UniformOnFun.ofFun_inv {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Inv β] (f : α → β) :
(ofFun 𝔖) f⁻¹ = ((ofFun 𝔖) f)⁻¹
source
@[simp]
theorem UniformOnFun.ofFun_neg {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Neg β] (f : α → β) :
(ofFun 𝔖) (-f) = -(ofFun 𝔖) f
source
instance instDivUniformFun {α : Type u_1} {β : Type u_2} [Div β] :
Div (UniformFun α β)
Equations

- instDivUniformFun = Pi.instDiv

source
instance instSubUniformFun {α : Type u_1} {β : Type u_2} [Sub β] :
Sub (UniformFun α β)
Equations

- instSubUniformFun = Pi.instSub

source
@[simp]
theorem UniformFun.toFun_div {α : Type u_1} {β : Type u_2} [Div β] (f g : UniformFun α β) :
toFun (f / g) = toFun f / toFun g
source
@[simp]
theorem UniformFun.toFun_sub {α : Type u_1} {β : Type u_2} [Sub β] (f g : UniformFun α β) :
toFun (f - g) = toFun f - toFun g
source
@[simp]
theorem UniformFun.ofFun_div {α : Type u_1} {β : Type u_2} [Div β] (f g : α → β) :
ofFun (f / g) = ofFun f / ofFun g
source
@[simp]
theorem UniformFun.ofFun_sub {α : Type u_1} {β : Type u_2} [Sub β] (f g : α → β) :
ofFun (f - g) = ofFun f - ofFun g
source
instance instDivUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Div β] :
Div (UniformOnFun α β 𝔖)
Equations

- instDivUniformOnFun = Pi.instDiv

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

- instSubUniformOnFun = Pi.instSub

source
@[simp]
theorem UniformOnFun.toFun_div {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Div β] (f g : UniformOnFun α β 𝔖) :
(toFun 𝔖) (f / g) = (toFun 𝔖) f / (toFun 𝔖) g
source
@[simp]
theorem UniformOnFun.toFun_sub {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Sub β] (f g : UniformOnFun α β 𝔖) :
(toFun 𝔖) (f - g) = (toFun 𝔖) f - (toFun 𝔖) g
source
@[simp]
theorem UniformOnFun.ofFun_div {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Div β] (f g : α → β) :
(ofFun 𝔖) (f / g) = (ofFun 𝔖) f / (ofFun 𝔖) g
source
@[simp]
theorem UniformOnFun.ofFun_sub {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Sub β] (f g : α → β) :
(ofFun 𝔖) (f - g) = (ofFun 𝔖) f - (ofFun 𝔖) g
source
instance instMonoidUniformFun {α : Type u_1} {β : Type u_2} [Monoid β] :
Monoid (UniformFun α β)
Equations

- instMonoidUniformFun = Pi.monoid

source
instance instAddMonoidUniformFun {α : Type u_1} {β : Type u_2} [AddMonoid β] :
AddMonoid (UniformFun α β)
Equations

- instAddMonoidUniformFun = Pi.addMonoid

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

- instMonoidUniformOnFun = Pi.monoid

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

- instAddMonoidUniformOnFun = Pi.addMonoid

source
instance instCommMonoidUniformFun {α : Type u_1} {β : Type u_2} [CommMonoid β] :
CommMonoid (UniformFun α β)
Equations

- instCommMonoidUniformFun = Pi.commMonoid

source
instance instAddCommMonoidUniformFun {α : Type u_1} {β : Type u_2} [AddCommMonoid β] :
AddCommMonoid (UniformFun α β)
Equations

- instAddCommMonoidUniformFun = Pi.addCommMonoid

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

- instCommMonoidUniformOnFun = Pi.commMonoid

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

- instAddCommMonoidUniformOnFun = Pi.addCommMonoid

source
instance instGroupUniformFun {α : Type u_1} {β : Type u_2} [Group β] :
Group (UniformFun α β)
Equations

- instGroupUniformFun = Pi.group

source
instance instAddGroupUniformFun {α : Type u_1} {β : Type u_2} [AddGroup β] :
AddGroup (UniformFun α β)
Equations

- instAddGroupUniformFun = Pi.addGroup

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

- instGroupUniformOnFun = Pi.group

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

- instAddGroupUniformOnFun = Pi.addGroup

source
instance instCommGroupUniformFun {α : Type u_1} {β : Type u_2} [CommGroup β] :
CommGroup (UniformFun α β)
Equations

- instCommGroupUniformFun = Pi.commGroup

source
instance instAddCommGroupUniformFun {α : Type u_1} {β : Type u_2} [AddCommGroup β] :
AddCommGroup (UniformFun α β)
Equations

- instAddCommGroupUniformFun = Pi.addCommGroup

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

- instCommGroupUniformOnFun = Pi.commGroup

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

- instAddCommGroupUniformOnFun = Pi.addCommGroup

source
instance instSMulUniformFun {α : Type u_1} {β : Type u_2} {M : Type u_5} [SMul M β] :
SMul M (UniformFun α β)
Equations

- instSMulUniformFun = Pi.instSMul

source
@[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
source
@[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
source
instance instSMulUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [SMul M β] :
SMul M (UniformOnFun α β 𝔖)
Equations

- instSMulUniformOnFun = Pi.instSMul

source
@[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
source
@[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
source
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 α β)
source
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 α β 𝔖)
source
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 α β)
source
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 α β 𝔖)
source
instance instMulActionUniformFun {α : Type u_1} {β : Type u_2} {M : Type u_5} [Monoid M] [MulAction M β] :
MulAction M (UniformFun α β)
Equations

- instMulActionUniformFun = Pi.mulAction M

source
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

source
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

source
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

source
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

source
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

source
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.

source
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.

source
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}
source
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}
source
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}
source
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}
source
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.

source
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.

source
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}
source
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}
source
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}
source
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}
source
@[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)
source
@[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)
source
@[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)
source
@[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)
source
@[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)
source
@[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)
source
@[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)
source
@[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)
source
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)
source
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 𝔖)