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 (⨅ (i : ι), UniformSpace.comap (fun (a : (i : ι) → α i) => a i) (U i))) Pi.topologicalSpace ⋯
theorem
Pi.uniformSpace_eq
{ι : Type u_1}
(α : ι → Type u)
[U : (i : ι) → UniformSpace (α i)]
:
Pi.uniformSpace α = ⨅ (i : ι), UniformSpace.comap (fun (a : (i : ι) → α i) => a 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
instIsCountablyGeneratedProdForAllUniformityUniformSpace
{ι : Type u_1}
{α : ι → Type u}
[U : (i : ι) → UniformSpace (α i)]
[Countable ι]
[∀ (i : ι), Filter.IsCountablyGenerated (uniformity (α i))]
:
Filter.IsCountablyGenerated (uniformity ((i : ι) → α i))
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 ι)
:
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 : ↑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)}
[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
- ⋯ = ⋯
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)
: