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: ifGis a uniform group, thenα →ᵤ Ga uniform groupUniformOnFun.uniform_group: ifGis a uniform group, then for any𝔖 : Set (Set α),α →ᵤ[𝔖] Ga 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][bourbaki1966]
- [N. Bourbaki, Topological Vector Spaces][bourbaki1987]
Tags #
uniform convergence, strong dual
Equations
Equations
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 β]
:
(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
Equations
Equations
@[simp]
@[simp]
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 α β 𝔖)
:
(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
Equations
Equations
@[simp]
@[simp]
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 α β 𝔖)
:
(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
Equations
Equations
@[simp]
@[simp]
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 α β 𝔖)
:
(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
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
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 α β)
:
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 α β 𝔖)
:
(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
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
- 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]
:
theorem
UniformFun.hasBasis_nhds_zero
{α : Type u_1}
{G : Type u_2}
[AddGroup G]
[UniformSpace G]
[UniformAddGroup G]
:
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) 𝔖)
:
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) 𝔖)
:
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 𝔖)