# Indexed product of uniform spaces #

source
instance Pi.uniformSpace {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] :
UniformSpace ((i : ι) → α i)
Equations

- Pi.uniformSpace α = UniformSpace.ofCoreEq (⨅ (i : ι), UniformSpace.comap (Function.eval i) (U i)).toCore Pi.topologicalSpace ⋯

source
theorem Pi.uniformSpace_eq {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] :
uniformSpace α = ⨅ (i : ι), UniformSpace.comap (Function.eval i) (U i)
source
theorem Pi.uniformity {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] :
_root_.uniformity ((i : ι) → α i) = ⨅ (i : ι), Filter.comap (fun (a : ((i : ι) → α i) × ((i : ι) → α i)) => (a.1 i, a.2 i)) (_root_.uniformity (α i))
source
instance instIsCountablyGeneratedProdForallUniformityOfCountable {ι : Type u_1} {α : ι → Type u} [U : (i : ι) → UniformSpace (α i)] [Countable ι] [∀ (i : ι), (uniformity (α i)).IsCountablyGenerated] :
(uniformity ((i : ι) → α i)).IsCountablyGenerated
source
theorem uniformContinuous_pi {ι : Type u_1} {α : ι → Type u} [U : (i : ι) → UniformSpace (α i)] {β : Type u_4} [UniformSpace β] {f : β → (i : ι) → α i} :
UniformContinuous f ↔ ∀ (i : ι), UniformContinuous fun (x : β) => f x i
source
theorem Pi.uniformContinuous_proj {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (i : ι) :
UniformContinuous fun (a : (i : ι) → α i) => a i
source
theorem Pi.uniformContinuous_precomp' {ι : Type u_1} {ι' : Type u_2} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (φ : ι' → ι) :
UniformContinuous fun (f : (i : ι) → α i) (j : ι') => f (φ j)
source
theorem Pi.uniformContinuous_precomp {ι : Type u_1} {ι' : Type u_2} {β : Type u_3} [UniformSpace β] (φ : ι' → ι) :
UniformContinuous fun (x : ι → β) => x ∘ φ
source
theorem Pi.uniformContinuous_postcomp' {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] {β : ι → Type u_4} [(i : ι) → UniformSpace (β i)] {g : (i : ι) → α i → β i} (hg : ∀ (i : ι), UniformContinuous (g i)) :
UniformContinuous fun (f : (i : ι) → α i) (i : ι) => g i (f i)
source
theorem Pi.uniformContinuous_postcomp {ι : Type u_1} {β : Type u_3} [UniformSpace β] {α : Type u_4} [UniformSpace α] {g : α → β} (hg : UniformContinuous g) :
UniformContinuous fun (x : ι → α) => g ∘ x
source
theorem Pi.uniformSpace_comap_precomp' {ι : Type u_1} {ι' : Type u_2} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (φ : ι' → ι) :
UniformSpace.comap (fun (g : (x : ι) → α x) (i' : ι') => g (φ i')) (uniformSpace fun (i' : ι') => α (φ i')) = ⨅ (i' : ι'), UniformSpace.comap (Function.eval (φ i')) (U (φ i'))
source
theorem Pi.uniformSpace_comap_precomp {ι : Type u_1} {ι' : Type u_2} {β : Type u_3} [UniformSpace β] (φ : ι' → ι) :
UniformSpace.comap (fun (x : ι → β) => x ∘ φ) (uniformSpace fun (x : ι') => β) = ⨅ (i' : ι'), UniformSpace.comap (Function.eval (φ i')) inst✝
source
theorem Pi.uniformContinuous_restrict {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (S : Set ι) :
UniformContinuous S.restrict
source
theorem Pi.uniformSpace_comap_restrict {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (S : Set ι) :
UniformSpace.comap S.restrict (uniformSpace fun (i : ↑S) => α ↑i) = ⨅ i ∈ S, UniformSpace.comap (Function.eval i) (U i)
source
theorem cauchy_pi_iff {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] [Nonempty ι] {l : Filter ((i : ι) → α i)} :
Cauchy l ↔ ∀ (i : ι), Cauchy (Filter.map (Function.eval i) l)
source
theorem cauchy_pi_iff' {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] {l : Filter ((i : ι) → α i)} [l.NeBot] :
Cauchy l ↔ ∀ (i : ι), Cauchy (Filter.map (Function.eval i) l)
source
theorem Cauchy.pi {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] [Nonempty ι] {l : (i : ι) → Filter (α i)} (hl : ∀ (i : ι), Cauchy (l i)) :
Cauchy (Filter.pi l)
source
instance Pi.complete {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] [∀ (i : ι), CompleteSpace (α i)] :
CompleteSpace ((i : ι) → α i)
source
theorem Pi.uniformSpace_comap_restrict_sUnion {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (𝔖 : Set (Set ι)) :
UniformSpace.comap (⋃₀ 𝔖).restrict (uniformSpace fun (i : ↑(⋃₀ 𝔖)) => α ↑i) = ⨅ S ∈ 𝔖, UniformSpace.comap S.restrict (uniformSpace fun (i : ↑S) => α ↑i)
source
theorem CompleteSpace.iInf {ι : Type u_4} {X : Type u_5} {u : ι → UniformSpace X} (hu : ∀ (i : ι), CompleteSpace X) (ht : ∃ (t : TopologicalSpace X), T2Space X ∧ ∀ (i : ι), (u i).toTopologicalSpace ≤ t) :
CompleteSpace X