Documentation

Mathlib.Topology.UniformSpace.Pi

Indexed product of uniform spaces #

instance Pi.uniformSpace {ι : Type u_1} (α : ιType u) [U : (i : ι) → UniformSpace (α i)] :
UniformSpace ((i : ι) → α i)
Equations
theorem Pi.uniformSpace_eq {ι : Type u_1} (α : ιType u) [U : (i : ι) → UniformSpace (α 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))
theorem instIsCountablyGeneratedProdForallUniformityOfCountable {ι : Type u_1} {α : ιType u} [U : (i : ι) → UniformSpace (α i)] [Countable ι] [∀ (i : ι), (uniformity (α i)).IsCountablyGenerated] :
(uniformity ((i : ι) → α i)).IsCountablyGenerated
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 ι) :
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) = iS, 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)) :
theorem Pi.complete {ι : Type u_1} (α : ιType u) [U : (i : ι) → UniformSpace (α i)] [∀ (i : ι), CompleteSpace (α i)] :
CompleteSpace ((i : ι) → α i)
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) :