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 #

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 #

Tags #

uniform convergence, strong dual

instance instZeroUniformFun {α : Type u_1} {β : Type u_2} [Zero β] :
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 β] :
@[simp]
theorem UniformOnFun.toFun_one {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [One β] :
@[simp]
theorem UniformOnFun.zero_apply {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Zero β] :
@[simp]
theorem UniformOnFun.one_apply {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [One β] :
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 α β 𝔖) :
@[simp]
theorem UniformOnFun.toFun_mul {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Mul β] (f : UniformOnFun α β 𝔖) (g : UniformOnFun α β 𝔖) :
@[simp]
theorem UniformOnFun.ofFun_add {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Add β] (f : αβ) (g : αβ) :
@[simp]
theorem UniformOnFun.ofFun_mul {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Mul β] (f : αβ) (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 α β 𝔖) :
@[simp]
theorem UniformOnFun.toFun_inv {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Inv β] (f : UniformOnFun α β 𝔖) :
@[simp]
theorem UniformOnFun.ofFun_neg {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Neg β] (f : αβ) :
@[simp]
theorem UniformOnFun.ofFun_inv {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Inv β] (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 α β 𝔖) :
@[simp]
theorem UniformOnFun.toFun_div {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Div β] (f : UniformOnFun α β 𝔖) (g : UniformOnFun α β 𝔖) :
@[simp]
theorem UniformOnFun.ofFun_sub {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Sub β] (f : αβ) (g : αβ) :
@[simp]
theorem UniformOnFun.ofFun_div {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Div β] (f : αβ) (g : αβ) :
instance instAddMonoidUniformFun {α : Type u_1} {β : Type u_2} [AddMonoid β] :
Equations
  • instAddMonoidUniformFun = Pi.addMonoid
instance instMonoidUniformFun {α : Type u_1} {β : Type u_2} [Monoid β] :
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 β] :
Equations
  • instAddCommMonoidUniformFun = Pi.addCommMonoid
instance instCommMonoidUniformFun {α : Type u_1} {β : Type u_2} [CommMonoid β] :
Equations
  • instCommMonoidUniformFun = Pi.commMonoid
instance instAddCommMonoidUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddCommMonoid β] :
Equations
  • instAddCommMonoidUniformOnFun = Pi.addCommMonoid
instance instCommMonoidUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [CommMonoid β] :
Equations
  • instCommMonoidUniformOnFun = Pi.commMonoid
instance instAddGroupUniformFun {α : Type u_1} {β : Type u_2} [AddGroup β] :
Equations
  • instAddGroupUniformFun = Pi.addGroup
instance instGroupUniformFun {α : Type u_1} {β : Type u_2} [Group β] :
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 β] :
Equations
  • instAddCommGroupUniformFun = Pi.addCommGroup
instance instCommGroupUniformFun {α : Type u_1} {β : Type u_2} [CommGroup β] :
Equations
  • instCommGroupUniformFun = Pi.commGroup
instance instAddCommGroupUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [AddCommGroup β] :
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 α β 𝔖) :
@[simp]
theorem UniformOnFun.ofFun_smul {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [SMul M β] (c : M) (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 β] :
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 β] :
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 β] :
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 β] :
Equations
instance instDistribMulActionUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {M : Type u_5} [Monoid M] [AddMonoid β] [DistribMulAction M β] :
Equations
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

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

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

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

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 (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 𝔖 | xSi.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 (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 𝔖 | xSi.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 (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 𝔖 | xSV.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 (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 𝔖 | xSV.1, f x SV.2}
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 α)} :
Equations
  • =