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.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
@[implicit_reducible]
@[implicit_reducible]
@[simp]
@[simp]
@[simp]
@[simp]
@[implicit_reducible]
instance
instOneUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[One β]
:
One (UniformOnFun α β 𝔖)
@[implicit_reducible]
instance
instZeroUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[Zero β]
:
Zero (UniformOnFun α β 𝔖)
@[simp]
@[simp]
@[simp]
@[simp]
@[implicit_reducible]
@[implicit_reducible]
@[simp]
@[simp]
@[simp]
@[simp]
@[implicit_reducible]
instance
instMulUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[Mul β]
:
Mul (UniformOnFun α β 𝔖)
@[implicit_reducible]
instance
instAddUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[Add β]
:
Add (UniformOnFun α β 𝔖)
@[simp]
theorem
UniformOnFun.toFun_mul
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[Mul β]
(f g : UniformOnFun α β 𝔖)
:
@[simp]
theorem
UniformOnFun.toFun_add
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[Add β]
(f g : UniformOnFun α β 𝔖)
:
@[simp]
@[simp]
@[implicit_reducible]
@[implicit_reducible]
@[simp]
@[simp]
@[simp]
@[simp]
@[implicit_reducible]
instance
instInvUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[Inv β]
:
Inv (UniformOnFun α β 𝔖)
@[implicit_reducible]
instance
instNegUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[Neg β]
:
Neg (UniformOnFun α β 𝔖)
@[simp]
theorem
UniformOnFun.toFun_inv
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[Inv β]
(f : UniformOnFun α β 𝔖)
:
@[simp]
theorem
UniformOnFun.toFun_neg
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[Neg β]
(f : UniformOnFun α β 𝔖)
:
@[implicit_reducible]
@[implicit_reducible]
@[simp]
@[simp]
@[simp]
@[simp]
@[implicit_reducible]
instance
instDivUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[Div β]
:
Div (UniformOnFun α β 𝔖)
@[implicit_reducible]
instance
instSubUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[Sub β]
:
Sub (UniformOnFun α β 𝔖)
@[simp]
theorem
UniformOnFun.toFun_div
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[Div β]
(f g : UniformOnFun α β 𝔖)
:
@[simp]
theorem
UniformOnFun.toFun_sub
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[Sub β]
(f g : UniformOnFun α β 𝔖)
:
@[simp]
@[simp]
@[implicit_reducible]
@[implicit_reducible]
instance
instAddMonoidUniformFun
{α : Type u_1}
{β : Type u_2}
[AddMonoid β]
:
AddMonoid (UniformFun α β)
@[implicit_reducible]
instance
instMonoidUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[Monoid β]
:
Monoid (UniformOnFun α β 𝔖)
@[implicit_reducible]
instance
instAddMonoidUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[AddMonoid β]
:
AddMonoid (UniformOnFun α β 𝔖)
@[implicit_reducible]
instance
instCommMonoidUniformFun
{α : Type u_1}
{β : Type u_2}
[CommMonoid β]
:
CommMonoid (UniformFun α β)
@[implicit_reducible]
instance
instAddCommMonoidUniformFun
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid β]
:
AddCommMonoid (UniformFun α β)
@[implicit_reducible]
instance
instCommMonoidUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[CommMonoid β]
:
CommMonoid (UniformOnFun α β 𝔖)
@[implicit_reducible]
instance
instAddCommMonoidUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[AddCommMonoid β]
:
AddCommMonoid (UniformOnFun α β 𝔖)
@[implicit_reducible]
@[implicit_reducible]
instance
instAddGroupUniformFun
{α : Type u_1}
{β : Type u_2}
[AddGroup β]
:
AddGroup (UniformFun α β)
@[implicit_reducible]
instance
instGroupUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[Group β]
:
Group (UniformOnFun α β 𝔖)
@[implicit_reducible]
instance
instAddGroupUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[AddGroup β]
:
AddGroup (UniformOnFun α β 𝔖)
@[implicit_reducible]
instance
instCommGroupUniformFun
{α : Type u_1}
{β : Type u_2}
[CommGroup β]
:
CommGroup (UniformFun α β)
@[implicit_reducible]
instance
instAddCommGroupUniformFun
{α : Type u_1}
{β : Type u_2}
[AddCommGroup β]
:
AddCommGroup (UniformFun α β)
@[implicit_reducible]
instance
instCommGroupUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[CommGroup β]
:
CommGroup (UniformOnFun α β 𝔖)
@[implicit_reducible]
instance
instAddCommGroupUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
[AddCommGroup β]
:
AddCommGroup (UniformOnFun α β 𝔖)
@[implicit_reducible]
instance
instSMulUniformFun
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[SMul M β]
:
SMul M (UniformFun α β)
@[simp]
theorem
UniformFun.toFun_smul
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[SMul M β]
(c : M)
(f : UniformFun α β)
:
@[simp]
@[implicit_reducible]
instance
instSMulUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
{M : Type u_5}
[SMul M β]
:
SMul M (UniformOnFun α β 𝔖)
@[simp]
theorem
UniformOnFun.toFun_smul
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
{M : Type u_5}
[SMul M β]
(c : M)
(f : UniformOnFun α β 𝔖)
:
@[simp]
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 α β 𝔖)
@[implicit_reducible]
instance
instMulActionUniformFun
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[Monoid M]
[MulAction M β]
:
MulAction M (UniformFun α β)
@[implicit_reducible]
instance
instMulActionUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
{M : Type u_5}
[Monoid M]
[MulAction M β]
:
MulAction M (UniformOnFun α β 𝔖)
@[implicit_reducible]
instance
instDistribMulActionUniformFun
{α : Type u_1}
{β : Type u_2}
{M : Type u_5}
[Monoid M]
[AddMonoid β]
[DistribMulAction M β]
:
DistribMulAction M (UniformFun α β)
@[implicit_reducible]
instance
instDistribMulActionUniformOnFun
{α : Type u_1}
{β : Type u_2}
{𝔖 : Set (Set α)}
{M : Type u_5}
[Monoid M]
[AddMonoid β]
[DistribMulAction M β]
:
DistribMulAction M (UniformOnFun α β 𝔖)
@[implicit_reducible]
instance
instModuleUniformFun
{α : Type u_1}
{β : Type u_2}
{R : Type u_4}
[Semiring R]
[AddCommMonoid β]
[Module R β]
:
Module R (UniformFun α β)
@[implicit_reducible]
instance
instModuleUniformOnFun
{α : Type u_1}
{β : Type u_2}
{R : Type u_4}
{𝔖 : Set (Set α)}
[Semiring R]
[AddCommMonoid β]
[Module R β]
:
Module R (UniformOnFun α β 𝔖)
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)
:
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)
:
theorem
UniformFun.hasBasis_nhds_one
{α : Type u_1}
{G : Type u_2}
[Group G]
[UniformSpace G]
[IsUniformGroup G]
:
theorem
UniformFun.hasBasis_nhds_zero
{α : Type u_1}
{G : Type u_2}
[AddGroup G]
[UniformSpace G]
[IsUniformAddGroup G]
:
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)
:
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)
:
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) 𝔖)
:
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) 𝔖)
:
@[simp]
theorem
UniformOnFun.ofFun_prod
{α : Type u_1}
{ι : Type u_3}
{𝔖 : Set (Set α)}
{β : Type u_4}
[CommMonoid β]
{f : ι → α → β}
(I : Finset ι)
:
@[simp]
theorem
UniformOnFun.ofFun_sum
{α : Type u_1}
{ι : Type u_3}
{𝔖 : Set (Set α)}
{β : Type u_4}
[AddCommMonoid β]
{f : ι → α → β}
(I : Finset ι)
:
@[simp]
theorem
UniformOnFun.toFun_prod
{α : Type u_1}
{ι : Type u_3}
{𝔖 : Set (Set α)}
{β : Type u_4}
[CommMonoid β]
{f : ι → α → β}
(I : Finset ι)
:
@[simp]
theorem
UniformOnFun.toFun_sum
{α : Type u_1}
{ι : Type u_3}
{𝔖 : Set (Set α)}
{β : Type u_4}
[AddCommMonoid β]
{f : ι → α → β}
(I : Finset ι)
:
@[simp]
theorem
UniformFun.ofFun_prod
{α : Type u_1}
{ι : Type u_3}
{β : Type u_4}
[CommMonoid β]
{f : ι → α → β}
(I : Finset ι)
:
@[simp]
theorem
UniformFun.ofFun_sum
{α : Type u_1}
{ι : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
{f : ι → α → β}
(I : Finset ι)
:
@[simp]
theorem
UniformFun.toFun_prod
{α : Type u_1}
{ι : Type u_3}
{β : Type u_4}
[CommMonoid β]
{f : ι → α → β}
(I : Finset ι)
:
@[simp]
theorem
UniformFun.toFun_sum
{α : Type u_1}
{ι : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
{f : ι → α → β}
(I : Finset ι)
:
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 𝔖)