Products of ultrametric (nonarchimedean) uniform spaces #
Main results #
IsUltraUniformity.prod: a product of uniform spaces with nonarchimedean uniformities has a nonarchimedean uniformity.IsUltraUniformity.pi: an indexed product of uniform spaces with nonarchimedean uniformities has a nonarchimedean uniformity.
Implementation details #
This file can be split to separate imports to have the Prod and Pi instances separately,
but would be somewhat unnatural since they are closely related.
The Prod instance only requires Mathlib/Topology/UniformSpace/Basic.lean.
theorem
IsTransitiveRel.entourageProd
{X : Type u_1}
{Y : Type u_2}
{s : Set (X × X)}
{t : Set (Y × Y)}
(hs : IsTransitiveRel s)
(ht : IsTransitiveRel t)
:
theorem
IsUltraUniformity.comap
{X : Type u_1}
{Y : Type u_2}
{u : UniformSpace Y}
(h : IsUltraUniformity Y)
(f : X → Y)
:
theorem
IsUltraUniformity.inf
{X : Type u_1}
{u u' : UniformSpace X}
(h : IsUltraUniformity X)
(h' : IsUltraUniformity X)
:
instance
IsUltraUniformity.prod
{X : Type u_1}
{Y : Type u_2}
[UniformSpace X]
[UniformSpace Y]
[IsUltraUniformity X]
[IsUltraUniformity Y]
:
IsUltraUniformity (X × Y)
The product of uniform spaces with nonarchimedean uniformities has a nonarchimedean uniformity.
theorem
IsUltraUniformity.iInf
{X : Type u_1}
{ι : Type u_3}
{U : ι → UniformSpace X}
(hU : ∀ (i : ι), IsUltraUniformity X)
:
instance
IsUltraUniformity.pi
{ι : Type u_3}
{X : ι → Type u_4}
[U : (i : ι) → UniformSpace (X i)]
[h : ∀ (i : ι), IsUltraUniformity (X i)]
:
IsUltraUniformity ((i : ι) → X i)
The indexed product of uniform spaces with nonarchimedean uniformities has a nonarchimedean uniformity.