Indexed product of uniform spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, instance]
def
Pi.uniform_space
{ι : Type u_1}
(α : ι → Type u)
[U : Π (i : ι), uniform_space (α i)] :
uniform_space (Π (i : ι), α i)
theorem
Pi.uniformity
{ι : Type u_1}
(α : ι → Type u)
[U : Π (i : ι), uniform_space (α i)] :
uniformity (Π (i : ι), α i) = ⨅ (i : ι), filter.comap (λ (a : (Π (i : ι), α i) × Π (i : ι), α i), (a.fst i, a.snd i)) (uniformity (α i))
theorem
uniform_continuous_pi
{ι : Type u_1}
{α : ι → Type u}
[U : Π (i : ι), uniform_space (α i)]
{β : Type u_2}
[uniform_space β]
{f : β → Π (i : ι), α i} :
uniform_continuous f ↔ ∀ (i : ι), uniform_continuous (λ (x : β), f x i)
theorem
Pi.uniform_continuous_proj
{ι : Type u_1}
(α : ι → Type u)
[U : Π (i : ι), uniform_space (α i)]
(i : ι) :
uniform_continuous (λ (a : Π (i : ι), α i), a i)
@[protected, instance]
def
Pi.complete
{ι : Type u_1}
(α : ι → Type u)
[U : Π (i : ι), uniform_space (α i)]
[∀ (i : ι), complete_space (α i)] :
complete_space (Π (i : ι), α i)
@[protected, instance]
def
Pi.separated
{ι : Type u_1}
(α : ι → Type u)
[U : Π (i : ι), uniform_space (α i)]
[∀ (i : ι), separated_space (α i)] :
separated_space (Π (i : ι), α i)