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, 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
• N. Bourbaki, Topological Vector Spaces

Tags

uniform convergence, strong dual

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

Equations

• instOneUniformFun = Pi.instOne

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

Equations

• instZeroUniformFun = Pi.instZero

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• instOneUniformOnFun = Pi.instOne

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

Equations

• instZeroUniformOnFun = Pi.instZero

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• instMulUniformFun = Pi.instMul

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

Equations

• instAddUniformFun = Pi.instAdd

@[simp]

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

@[simp]

theorem UniformFun.toFun_add {α : Type u_1} {β : Type u_2} [Add β] (f g : UniformFun α β) : UniformFun.toFun (f + g) = UniformFun.toFun f + UniformFun.toFun 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

@[simp]

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

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

Equations

• instMulUniformOnFun = Pi.instMul

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

Equations

• instAddUniformOnFun = Pi.instAdd

@[simp]

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

@[simp]

theorem UniformOnFun.toFun_add {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Add β] (f g : UniformOnFun α β 𝔖) : (UniformOnFun.toFun 𝔖) (f + g) = (UniformOnFun.toFun 𝔖) f + (UniformOnFun.toFun 𝔖) 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

@[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

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

Equations

• instInvUniformFun = Pi.instInv

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

Equations

• instNegUniformFun = Pi.instNeg

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• instInvUniformOnFun = Pi.instInv

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

Equations

• instNegUniformOnFun = Pi.instNeg

@[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.toFun_neg {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Neg β] (f : UniformOnFun α β 𝔖) : (UniformOnFun.toFun 𝔖) (-f) = -(UniformOnFun.toFun 𝔖) f

@[simp]

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

@[simp]

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

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

Equations

• instDivUniformFun = Pi.instDiv

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

Equations

• instSubUniformFun = Pi.instSub

@[simp]

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

@[simp]

theorem UniformFun.toFun_sub {α : Type u_1} {β : Type u_2} [Sub β] (f g : UniformFun α β) : UniformFun.toFun (f - g) = UniformFun.toFun f - UniformFun.toFun 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

@[simp]

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

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

Equations

• instDivUniformOnFun = Pi.instDiv

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

Equations

• instSubUniformOnFun = Pi.instSub

@[simp]

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

@[simp]

theorem UniformOnFun.toFun_sub {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Sub β] (f g : UniformOnFun α β 𝔖) : (UniformOnFun.toFun 𝔖) (f - g) = (UniformOnFun.toFun 𝔖) f - (UniformOnFun.toFun 𝔖) 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

@[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

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

Equations

• instMonoidUniformFun = Pi.monoid

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

Equations

• instAddMonoidUniformFun = Pi.addMonoid

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

Equations

• instMonoidUniformOnFun = Pi.monoid

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

Equations

• instAddMonoidUniformOnFun = Pi.addMonoid

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

Equations

• instCommMonoidUniformFun = Pi.commMonoid

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

Equations

• instAddCommMonoidUniformFun = Pi.addCommMonoid

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

Equations

• instCommMonoidUniformOnFun = Pi.commMonoid

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

Equations

• instAddCommMonoidUniformOnFun = Pi.addCommMonoid

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

Equations

• instGroupUniformFun = Pi.group

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

Equations

• instAddGroupUniformFun = Pi.addGroup

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

Equations

• instGroupUniformOnFun = Pi.group

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

Equations

• instAddGroupUniformOnFun = Pi.addGroup

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

Equations

• instCommGroupUniformFun = Pi.commGroup

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

Equations

• instAddCommGroupUniformFun = Pi.addCommGroup

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

Equations

• instCommGroupUniformOnFun = Pi.commGroup

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

Equations

• instAddCommGroupUniformOnFun = Pi.addCommGroup

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

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

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

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.

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_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 {α : 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}

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}

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.

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.

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 (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, (UniformOnFun.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] [UniformAddGroup 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, (UniformOnFun.toFun 𝔖) f x ∈ b Si.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 (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] [UniformAddGroup 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}

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