Indexed product of uniform spaces

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 ⋯

theorem Pi.uniformSpace_eq {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] : Pi.uniformSpace α = ⨅ (i : ι), UniformSpace.comap (Function.eval i) (U i)

theorem Pi.uniformity {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] : uniformity ((i : ι) → α i) = ⨅ (i : ι), Filter.comap (fun (a : ((i : ι) → α i) × ((i : ι) → α i)) => (a.1 i, a.2 i)) (uniformity (α i))

instance instIsCountablyGeneratedProdForallUniformityOfCountable {ι : Type u_1} {α : ι → Type u} [U : (i : ι) → UniformSpace (α i)] [Countable ι] [∀ (i : ι), (uniformity (α i)).IsCountablyGenerated] : (uniformity ((i : ι) → α i)).IsCountablyGenerated

Equations

• ⋯ = ⋯

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

theorem Pi.uniformContinuous_proj {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (i : ι) : UniformContinuous fun (a : (i : ι) → α i) => a i

theorem Pi.uniformContinuous_precomp' {ι : Type u_1} {ι' : Type u_2} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (φ : ι' → ι) : UniformContinuous fun (f : (i : ι) → α i) (j : ι') => f (φ j)

theorem Pi.uniformContinuous_precomp {ι : Type u_1} {ι' : Type u_2} {β : Type u_3} [UniformSpace β] (φ : ι' → ι) : UniformContinuous fun (x : ι → β) => x ∘ φ

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)

theorem Pi.uniformContinuous_postcomp {ι : Type u_1} {β : Type u_3} [UniformSpace β] {α : Type u_4} [UniformSpace α] {g : α → β} (hg : UniformContinuous g) : UniformContinuous fun (x : ι → α) => g ∘ x

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')) (Pi.uniformSpace fun (i' : ι') => α (φ i')) = ⨅ (i' : ι'), UniformSpace.comap (Function.eval (φ i')) (U (φ i'))

theorem Pi.uniformSpace_comap_precomp {ι : Type u_1} {ι' : Type u_2} {β : Type u_3} [UniformSpace β] (φ : ι' → ι) : UniformSpace.comap (fun (x : ι → β) => x ∘ φ) (Pi.uniformSpace fun (x : ι') => β) = ⨅ (i' : ι'), UniformSpace.comap (Function.eval (φ i')) inst✝

theorem Pi.uniformContinuous_restrict {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (S : Set ι) : UniformContinuous S.restrict

theorem Pi.uniformSpace_comap_restrict {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (S : Set ι) : UniformSpace.comap S.restrict (Pi.uniformSpace fun (i : ↑S) => α ↑i) = ⨅ i ∈ S, UniformSpace.comap (Function.eval i) (U i)

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)

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)

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)

instance Pi.complete {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] [∀ (i : ι), CompleteSpace (α i)] : CompleteSpace ((i : ι) → α i)

Equations

• ⋯ = ⋯

theorem Pi.uniformSpace_comap_restrict_sUnion {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (𝔖 : Set (Set ι)) : UniformSpace.comap (⋃₀ 𝔖).restrict (Pi.uniformSpace fun (i : ↑(⋃₀ 𝔖)) => α ↑i) = ⨅ S ∈ 𝔖, UniformSpace.comap S.restrict (Pi.uniformSpace fun (i : ↑S) => α ↑i)

theorem CompleteSpace.iInf {ι : Type u_4} {X : Type u_5} {u : ι → UniformSpace X} (hu : ∀ (i : ι), CompleteSpace X) (ht : ∃ (t : TopologicalSpace X), T2Space X ∧ ∀ (i : ι), UniformSpace.toTopologicalSpace ≤ t) : CompleteSpace X