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 UniformSpace.toCore Pi.topologicalSpace (_ : Pi.topologicalSpace = UniformSpace.Core.toTopologicalSpace UniformSpace.toCore)
theorem
Pi.uniformSpace_eq
{ι : Type u_1}
(α : ι → Type u)
[U : (i : ι) → UniformSpace (α i)]
:
Pi.uniformSpace α = ⨅ (i : ι), UniformSpace.comap (fun a => a i) (U i)
theorem
Pi.uniformity
{ι : Type u_1}
(α : ι → Type u)
[U : (i : ι) → UniformSpace (α i)]
:
uniformity ((i : ι) → α i) = ⨅ (i : ι),
Filter.comap (fun a => (Prod.fst ((i : ι) → α i) ((i : ι) → α i) a i, Prod.snd ((i : ι) → α i) ((i : ι) → α i) a i))
(uniformity (α i))
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 => a i
theorem
Pi.uniformContinuous_precomp'
{ι : Type u_1}
{ι' : Type u_2}
(α : ι → Type u)
[U : (i : ι) → UniformSpace (α i)]
(φ : ι' → ι)
:
UniformContinuous fun f 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 => 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 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 (Set.restrict S) (Pi.uniformSpace fun i => α ↑i) = ⨅ (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)}
[Filter.NeBot l]
:
Cauchy l ↔ ∀ (i : ι), Cauchy (Filter.map (Function.eval i) l)
instance
Pi.complete
{ι : Type u_1}
(α : ι → Type u)
[U : (i : ι) → UniformSpace (α i)]
[∀ (i : ι), CompleteSpace (α i)]
:
CompleteSpace ((i : ι) → α i)
Equations
instance
Pi.separated
{ι : Type u_1}
(α : ι → Type u)
[U : (i : ι) → UniformSpace (α i)]
[∀ (i : ι), SeparatedSpace (α i)]
:
SeparatedSpace ((i : ι) → α i)