mathlib documentation

topology.uniform_space.pi

Indexed product of uniform spaces #

source
@[protected, instance]
def Pi.uniform_space {ι : Type u_1} (α : ι → Type u) [U : Π (i : ι), uniform_space (α i)] :
uniform_space (Π (i : ι), α i)
Equations
source
theorem Pi.uniformity {ι : Type u_1} (α : ι → Type u) [U : Π (i : ι), uniform_space (α i)] :
𝓤 (Π (i : ι), α i) = ⨅ (i : ι), filter.comap (λ (a : (Π (i : ι), α i) × Π (i : ι), α i), (a.fst i, a.snd i)) (𝓤 (α i))
source
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)
source
theorem Pi.uniform_continuous_proj {ι : Type u_1} (α : ι → Type u) [U : Π (i : ι), uniform_space (α i)] (i : ι) :
uniform_continuous (λ (a : Π (i : ι), α i), a i)
source
@[protected, instance]
def Pi.complete {ι : Type u_1} (α : ι → Type u) [U : Π (i : ι), uniform_space (α i)] [∀ (i : ι), complete_space (α i)] :
complete_space (Π (i : ι), α i)
source
@[protected, instance]
def Pi.separated {ι : Type u_1} (α : ι → Type u) [U : Π (i : ι), uniform_space (α i)] [∀ (i : ι), separated_space (α i)] :
separated_space (Π (i : ι), α i)