Mathlib.Topology.UniformSpace.Pi

Pi.uniformSpace instance

: UniformSpace (∀ i, α i)

Full source

instance Pi.uniformSpace : UniformSpace (∀ i, α i) :=
  UniformSpace.ofCoreEq (⨅ i, UniformSpace.comap (eval i) (U i)).toCore
      Pi.topologicalSpace <|
    Eq.symm toTopologicalSpace_iInf

Uniform Space Structure on Product of Uniform Spaces

Informal description

The product space $\prod_{i} \alpha_i$ of a family of uniform spaces $\{\alpha_i\}_{i \in \iota}$ is equipped with the uniform space structure given by the infimum of the pullback uniformities under the evaluation maps $\mathrm{eval}_i \colon \prod_{i} \alpha_i \to \alpha_i$ for each $i \in \iota$. This means that the uniformity on the product space is the coarsest uniformity making all the evaluation maps uniformly continuous.

Pi.uniformSpace_eq theorem

: Pi.uniformSpace α = ⨅ i, UniformSpace.comap (eval i) (U i)

Full source

lemma Pi.uniformSpace_eq :
    Pi.uniformSpace α = ⨅ i, UniformSpace.comap (eval i) (U i) := by
  ext : 1; rfl

Product Uniformity as Infimum of Pullback Uniformities

Informal description

The uniform space structure on the product space $\prod_{i} \alpha_i$ of a family of uniform spaces $\{\alpha_i\}_{i \in \iota}$ is equal to the infimum of the pullback uniformities under the evaluation maps $\mathrm{eval}_i \colon \prod_{i} \alpha_i \to \alpha_i$ for each $i \in \iota$. In other words, the uniformity on the product space is the coarsest uniformity that makes all evaluation maps uniformly continuous.

Pi.uniformity theorem

: 𝓤 (∀ i, α i) = ⨅ i : ι, (Filter.comap fun a => (a.1 i, a.2 i)) (𝓤 (α i))

Full source

theorem Pi.uniformity :
    𝓤 (∀ i, α i) = ⨅ i : ι, (Filter.comap fun a => (a.1 i, a.2 i)) (𝓤 (α i)) :=
  iInf_uniformity

Uniformity of Product Space as Infimum of Pullback Uniformities

Informal description

For a family of uniform spaces $\{\alpha_i\}_{i \in \iota}$, the uniformity filter on the product space $\prod_{i} \alpha_i$ is equal to the infimum of the pullback filters of the uniformity filters $\mathfrak{U}(\alpha_i)$ under the coordinate projections. More precisely, \[ \mathfrak{U}\left(\prod_{i} \alpha_i\right) = \bigsqcap_{i \in \iota} \text{comap}\, (\lambda a \mapsto (a.1 i, a.2 i))\, \mathfrak{U}(\alpha_i), \] where $\text{comap}$ denotes the pullback of filters under the given map.

instIsCountablyGeneratedProdForallUniformityOfCountable instance

[Countable ι] [∀ i, IsCountablyGenerated (𝓤 (α i))] : IsCountablyGenerated (𝓤 (∀ i, α i))

Full source

instance [Countable ι] [∀ i, IsCountablyGenerated (𝓤 (α i))] :
    IsCountablyGenerated (𝓤 (∀ i, α i)) := by
  rw [Pi.uniformity]
  infer_instance

Countable Generation of Uniformity in Product Spaces

Informal description

For a countable index set $\iota$ and a family of uniform spaces $\{\alpha_i\}_{i \in \iota}$ where each uniformity filter $\mathfrak{U}(\alpha_i)$ is countably generated, the uniformity filter on the product space $\prod_{i} \alpha_i$ is also countably generated.

uniformContinuous_pi theorem

 {β : Type*} [UniformSpace β] {f : β → ∀ i, α i} : UniformContinuous f ↔ ∀ i, UniformContinuous fun x => f x i

Full source

theorem uniformContinuous_pi {β : Type*} [UniformSpace β] {f : β → ∀ i, α i} :
    UniformContinuousUniformContinuous f ↔ ∀ i, UniformContinuous fun x => f x i := by
  simp only [UniformContinuous, Pi.uniformity, tendsto_iInf, tendsto_comap_iff, Function.comp_def]

Uniform Continuity of a Function into a Product Space via Coordinate Functions

Informal description

Let $\{\alpha_i\}_{i \in \iota}$ be a family of uniform spaces, $\beta$ be a uniform space, and $f \colon \beta \to \prod_{i \in \iota} \alpha_i$ be a function. Then $f$ is uniformly continuous if and only if for each $i \in \iota$, the coordinate function $x \mapsto f(x)_i$ is uniformly continuous.

Pi.uniformContinuous_proj theorem

(i : ι) : UniformContinuous fun a : ∀ i : ι, α i => a i

Full source

theorem Pi.uniformContinuous_proj (i : ι) : UniformContinuous fun a : ∀ i : ι, α i => a i :=
  uniformContinuous_pi.1 uniformContinuous_id i

Uniform Continuity of Projection Maps in Product Uniform Spaces

Informal description

For any index $i$ in the index set $\iota$, the projection map $\pi_i \colon \prod_{j \in \iota} \alpha_j \to \alpha_i$ defined by $\pi_i(a) = a_i$ is uniformly continuous.

Pi.uniformContinuous_precomp' theorem

(φ : ι' → ι) : UniformContinuous (fun (f : (∀ i, α i)) (j : ι') ↦ f (φ j))

Full source

theorem Pi.uniformContinuous_precomp' (φ : ι' → ι) :
    UniformContinuous (fun (f : (∀ i, α i)) (j : ι') ↦ f (φ j)) :=
  uniformContinuous_pi.mpr fun j ↦ uniformContinuous_proj α (φ j)

Uniform Continuity of Precomposition in Product Uniform Spaces

Informal description

Let $\{\alpha_i\}_{i \in \iota}$ be a family of uniform spaces, and let $\varphi \colon \iota' \to \iota$ be a function between index sets. Then the precomposition map \[ f \mapsto (j \mapsto f(\varphi(j))) \] from $\prod_{i \in \iota} \alpha_i$ to $\prod_{j \in \iota'} \alpha_{\varphi(j)}$ is uniformly continuous.

Pi.uniformContinuous_precomp theorem

(φ : ι' → ι) : UniformContinuous (· ∘ φ : (ι → β) → (ι' → β))

Full source

theorem Pi.uniformContinuous_precomp (φ : ι' → ι) :
    UniformContinuous (· ∘ φ : (ι → β) → (ι' → β)) :=
  Pi.uniformContinuous_precomp' _ φ

Uniform Continuity of Precomposition in Product Uniform Spaces

Informal description

Let $\{\beta_i\}_{i \in \iota}$ be a family of uniform spaces, and let $\varphi \colon \iota' \to \iota$ be a function between index sets. Then the precomposition map \[ f \mapsto f \circ \varphi \] from the product space $\prod_{i \in \iota} \beta_i$ to $\prod_{j \in \iota'} \beta_{\varphi(j)}$ is uniformly continuous.

Pi.uniformContinuous_postcomp' theorem

 {β : ι → Type*} [∀ i, UniformSpace (β i)] {g : ∀ i, α i → β i} (hg : ∀ i, UniformContinuous (g i)) :
  UniformContinuous (fun (f : (∀ i, α i)) (i : ι) ↦ g i (f i))

Full source

theorem Pi.uniformContinuous_postcomp' {β : ι → Type*} [∀ i, UniformSpace (β i)]
    {g : ∀ i, α i → β i} (hg : ∀ i, UniformContinuous (g i)) :
    UniformContinuous (fun (f : (∀ i, α i)) (i : ι) ↦ g i (f i)) :=
  uniformContinuous_pi.mpr fun i ↦ (hg i).comp <| uniformContinuous_proj α i

Uniform Continuity of Postcomposition in Product Uniform Spaces

Informal description

Let $\{\alpha_i\}_{i \in \iota}$ and $\{\beta_i\}_{i \in \iota}$ be families of uniform spaces, and for each $i \in \iota$, let $g_i \colon \alpha_i \to \beta_i$ be a uniformly continuous function. Then the function $f \mapsto (i \mapsto g_i(f(i)))$ from $\prod_{i \in \iota} \alpha_i$ to $\prod_{i \in \iota} \beta_i$ is uniformly continuous.

Pi.uniformContinuous_postcomp theorem

 {α : Type*} [UniformSpace α] {g : α → β} (hg : UniformContinuous g) : UniformContinuous (g ∘ · : (ι → α) → (ι → β))

Full source

theorem Pi.uniformContinuous_postcomp {α : Type*} [UniformSpace α] {g : α → β}
    (hg : UniformContinuous g) : UniformContinuous (g ∘ · : (ι → α) → (ι → β)) :=
  Pi.uniformContinuous_postcomp' _ fun _ ↦ hg

Uniform Continuity of Postcomposition in Function Space

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, and let $g \colon \alpha \to \beta$ be a uniformly continuous function. Then the function $f \mapsto g \circ f$ from $\iota \to \alpha$ to $\iota \to \beta$ is uniformly continuous with respect to the product uniformities.

Pi.uniformSpace_comap_precomp' theorem

 (φ : ι' → ι) :
  UniformSpace.comap (fun g i' ↦ g (φ i')) (Pi.uniformSpace (fun i' ↦ α (φ i'))) =
    ⨅ i', UniformSpace.comap (eval (φ i')) (U (φ i'))

Full source

lemma Pi.uniformSpace_comap_precomp' (φ : ι' → ι) :
    UniformSpace.comap (fun g i' ↦ g (φ i')) (Pi.uniformSpace (fun i' ↦ α (φ i'))) =
    ⨅ i', UniformSpace.comap (eval (φ i')) (U (φ i')) := by
  simp [Pi.uniformSpace_eq, UniformSpace.comap_iInf, ← UniformSpace.comap_comap, comp_def]

Pullback of Product Uniformity via Precomposition Equals Infimum of Pullback Uniformities

Informal description

For any function $\phi \colon \iota' \to \iota$ between index sets, the pullback uniform space structure on $\prod_{i'} \alpha_{\phi(i')}$ via the precomposition map $g \mapsto (i' \mapsto g(\phi(i')))$ is equal to the infimum of the pullback uniformities under the evaluation maps $\mathrm{eval}_{\phi(i')} \colon \prod_{i'} \alpha_{\phi(i')} \to \alpha_{\phi(i')}$ for each $i' \in \iota'$. That is, \[ \mathrm{comap}\, \big(g \mapsto (i' \mapsto g(\phi(i')))\big) \left( \prod_{i'} \alpha_{\phi(i')} \right) = \bigsqcap_{i'} \mathrm{comap}\, (\mathrm{eval}_{\phi(i')}) \left( U_{\phi(i')} \right). \]

Pi.uniformSpace_comap_precomp theorem

 (φ : ι' → ι) :
  UniformSpace.comap (· ∘ φ) (Pi.uniformSpace (fun _ ↦ β)) = ⨅ i', UniformSpace.comap (eval (φ i')) ‹UniformSpace β›

Full source

lemma Pi.uniformSpace_comap_precomp (φ : ι' → ι) :
    UniformSpace.comap (· ∘ φ) (Pi.uniformSpace (fun _ ↦ β)) =
    ⨅ i', UniformSpace.comap (eval (φ i')) ‹UniformSpace β› :=
  uniformSpace_comap_precomp' (fun _ ↦ β) φ

Pullback of Product Uniformity via Precomposition Equals Infimum of Evaluation Pullbacks

Informal description

For any function $\phi \colon \iota' \to \iota$ between index sets, the pullback uniform space structure on $\prod_{i'} \beta$ via the precomposition map $f \mapsto f \circ \phi$ is equal to the infimum of the pullback uniformities under the evaluation maps $\mathrm{eval}_{\phi(i')} \colon \prod_{i'} \beta \to \beta$ for each $i' \in \iota'$. That is, \[ \mathrm{comap}\, (\cdot \circ \phi) \left( \prod_{i'} \beta \right) = \bigsqcap_{i'} \mathrm{comap}\, (\mathrm{eval}_{\phi(i')}) \left( \mathcal{U}_\beta \right), \] where $\mathcal{U}_\beta$ denotes the uniformity on $\beta$.

Pi.uniformContinuous_restrict theorem

(S : Set ι) : UniformContinuous (S.restrict : (∀ i : ι, α i) → (∀ i : S, α i))

Full source

lemma Pi.uniformContinuous_restrict (S : Set ι) :
    UniformContinuous (S.restrict : (∀ i : ι, α i) → (∀ i : S, α i)) :=
  Pi.uniformContinuous_precomp' _ ((↑) : S → ι)

Uniform Continuity of Restriction Map in Product Uniform Spaces

Informal description

For any subset $S$ of an index set $\iota$ and a family of uniform spaces $\{\alpha_i\}_{i \in \iota}$, the restriction map \[ f \mapsto f|_S \] from the product space $\prod_{i \in \iota} \alpha_i$ to $\prod_{i \in S} \alpha_i$ is uniformly continuous.

Pi.uniformSpace_comap_restrict theorem

 (S : Set ι) :
  UniformSpace.comap (S.restrict) (Pi.uniformSpace (fun i : S ↦ α i)) = ⨅ i ∈ S, UniformSpace.comap (eval i) (U i)

Full source

lemma Pi.uniformSpace_comap_restrict (S : Set ι) :
    UniformSpace.comap (S.restrict) (Pi.uniformSpace (fun i : S ↦ α i)) =
    ⨅ i ∈ S, UniformSpace.comap (eval i) (U i) := by
  simp +unfoldPartialApp
    [← iInf_subtype'', ← uniformSpace_comap_precomp' _ ((↑) : S → ι), Set.restrict]

Pullback of Product Uniformity via Restriction Equals Infimum of Pullback Uniformities over Subset

Informal description

For any subset $S$ of an index set $\iota$ and a family of uniform spaces $\{\alpha_i\}_{i \in \iota}$, the pullback uniform space structure on the product space $\prod_{i \in S} \alpha_i$ via the restriction map $S.\mathrm{restrict} \colon \prod_{i \in \iota} \alpha_i \to \prod_{i \in S} \alpha_i$ is equal to the infimum of the pullback uniformities under the evaluation maps $\mathrm{eval}_i \colon \prod_{i \in \iota} \alpha_i \to \alpha_i$ for each $i \in S$. That is, \[ \mathrm{comap}\, (S.\mathrm{restrict}) \left( \prod_{i \in S} \alpha_i \right) = \bigsqcap_{i \in S} \mathrm{comap}\, (\mathrm{eval}_i) (U_i). \]

cauchy_pi_iff theorem

[Nonempty ι] {l : Filter (∀ i, α i)} : Cauchy l ↔ ∀ i, Cauchy (map (eval i) l)

Full source

lemma cauchy_pi_iff [Nonempty ι] {l : Filter (∀ i, α i)} :
    CauchyCauchy l ↔ ∀ i, Cauchy (map (eval i) l) := by
  simp_rw [Pi.uniformSpace_eq, cauchy_iInf_uniformSpace, cauchy_comap_uniformSpace]

Cauchy Criterion for Product Filters in Uniform Spaces

Informal description

Let $\{\alpha_i\}_{i \in \iota}$ be a family of uniform spaces indexed by a nonempty set $\iota$, and let $l$ be a filter on the product space $\prod_{i \in \iota} \alpha_i$. Then $l$ is a Cauchy filter if and only if for every index $i \in \iota$, the pushforward filter $\mathrm{eval}_i(l)$ is a Cauchy filter on $\alpha_i$.

cauchy_pi_iff' theorem

{l : Filter (∀ i, α i)} [l.NeBot] : Cauchy l ↔ ∀ i, Cauchy (map (eval i) l)

Full source

lemma cauchy_pi_iff' {l : Filter (∀ i, α i)} [l.NeBot] :
    CauchyCauchy l ↔ ∀ i, Cauchy (map (eval i) l) := by
  simp_rw [Pi.uniformSpace_eq, cauchy_iInf_uniformSpace', cauchy_comap_uniformSpace]

Cauchy Criterion for Product Uniform Spaces: $l$ is Cauchy iff all projections are Cauchy

Informal description

Let $\{\alpha_i\}_{i \in \iota}$ be a family of uniform spaces, and let $l$ be a nontrivial filter on the product space $\prod_{i} \alpha_i$. Then $l$ is a Cauchy filter if and only if for every index $i$, the pushforward filter $\mathrm{eval}_i(l)$ is a Cauchy filter on $\alpha_i$.

Cauchy.pi theorem

[Nonempty ι] {l : ∀ i, Filter (α i)} (hl : ∀ i, Cauchy (l i)) : Cauchy (Filter.pi l)

Full source

lemma Cauchy.pi [Nonempty ι] {l : ∀ i, Filter (α i)} (hl : ∀ i, Cauchy (l i)) :
    Cauchy (Filter.pi l) := by
  have := fun i ↦ (hl i).1
  simpa [cauchy_pi_iff]

Cauchy Property of Product Filters in Uniform Spaces

Informal description

Let $\{\alpha_i\}_{i \in \iota}$ be a family of uniform spaces indexed by a nonempty set $\iota$, and let $\{l_i\}_{i \in \iota}$ be a family of filters where each $l_i$ is a Cauchy filter on $\alpha_i$. Then the product filter $\prod_{i \in \iota} l_i$ is a Cauchy filter on the product space $\prod_{i \in \iota} \alpha_i$.

Pi.complete instance

[∀ i, CompleteSpace (α i)] : CompleteSpace (∀ i, α i)

Full source

instance Pi.complete [∀ i, CompleteSpace (α i)] : CompleteSpace (∀ i, α i) where
  complete {f} hf := by
    have := hf.1
    simp_rw [cauchy_pi_iff', cauchy_iff_exists_le_nhds] at hf
    choose x hx using hf
    use x
    rwa [nhds_pi, le_pi]

Completeness of Product of Complete Uniform Spaces

Informal description

For any family of uniform spaces $\{\alpha_i\}_{i \in \iota}$ where each $\alpha_i$ is a complete space, the product space $\prod_{i} \alpha_i$ is also a complete space.

Pi.uniformSpace_comap_restrict_sUnion theorem

 (𝔖 : Set (Set ι)) :
  UniformSpace.comap (⋃₀ 𝔖).restrict (Pi.uniformSpace (fun i : (⋃₀ 𝔖) ↦ α i)) =
    ⨅ S ∈ 𝔖, UniformSpace.comap S.restrict (Pi.uniformSpace (fun i : S ↦ α i))

Full source

lemma Pi.uniformSpace_comap_restrict_sUnion (𝔖 : Set (Set ι)) :
    UniformSpace.comap (⋃₀ 𝔖).restrict (Pi.uniformSpace (fun i : (⋃₀ 𝔖) ↦ α i)) =
    ⨅ S ∈ 𝔖, UniformSpace.comap S.restrict (Pi.uniformSpace (fun i : S ↦ α i)) := by
  simp_rw [Pi.uniformSpace_comap_restrict α, iInf_sUnion]

Pullback of Product Uniformity via Union Restriction Equals Infimum of Pullback Uniformities over Subsets

Informal description

For any family $\mathfrak{S}$ of subsets of an index set $\iota$ and a family of uniform spaces $\{\alpha_i\}_{i \in \iota}$, the pullback uniform space structure on the product space $\prod_{i \in \bigcup \mathfrak{S}} \alpha_i$ via the restriction map $(\bigcup \mathfrak{S}).\mathrm{restrict}$ is equal to the infimum of the pullback uniformities under the restriction maps $S.\mathrm{restrict} \colon \prod_{i \in \iota} \alpha_i \to \prod_{i \in S} \alpha_i$ for each $S \in \mathfrak{S}$. In symbols: \[ \mathrm{comap}\, \left((\bigcup \mathfrak{S}).\mathrm{restrict}\right) \left( \prod_{i \in \bigcup \mathfrak{S}} \alpha_i \right) = \bigsqcap_{S \in \mathfrak{S}} \mathrm{comap}\, (S.\mathrm{restrict}) \left( \prod_{i \in S} \alpha_i \right). \]

CompleteSpace.iInf theorem

 {ι X : Type*} {u : ι → UniformSpace X} (hu : ∀ i, @CompleteSpace X (u i))
  (ht : ∃ t, @T2Space X t ∧ ∀ i, (u i).toTopologicalSpace ≤ t) : @CompleteSpace X (⨅ i, u i)

Full source

protected theorem CompleteSpace.iInf {ι X : Type*} {u : ι → UniformSpace X}
    (hu : ∀ i, @CompleteSpace X (u i))
    (ht : ∃ t, @T2Space X t ∧ ∀ i, (u i).toTopologicalSpace ≤ t) :
    @CompleteSpace X (⨅ i, u i) := by
  -- We can assume `X` is nonempty.
  nontriviality X
  rcases ht with ⟨t, ht, hut⟩
  -- The diagonal map `(X, ⨅ i, u i) → ∀ i, (X, u i)` is a uniform embedding.
  have : @IsUniformInducing X (ι → X) (⨅ i, u i) (Pi.uniformSpace (U := u)) (const ι) := by
    simp_rw [isUniformInducing_iff, iInf_uniformity, Pi.uniformity, Filter.comap_iInf,
      Filter.comap_comap, comp_def, const, Prod.eta, comap_id']
  -- Hence, it suffices to show that its range, the diagonal, is closed in `Π i, (X, u i)`.
  simp_rw [@completeSpace_iff_isComplete_range _ _ (_) (_) _ this, range_const_eq_diagonal,
    setOf_forall]
  -- The separation of `t` ensures that this is the case in `Π i, (X, t)`, hence the result
  -- since the topology associated to each `u i` is finer than `t`.
  have : Pi.topologicalSpace (t₂ := fun i ↦ (u i).toTopologicalSpace) ≤
         Pi.topologicalSpace (t₂ := fun _ ↦ t) :=
    iInf_mono fun i ↦ induced_mono <| hut i
  refine IsClosed.isComplete <| .mono ?_ this
  exact isClosed_iInter fun i ↦ isClosed_iInter fun j ↦
    isClosed_eq (continuous_apply _) (continuous_apply _)

Completeness of Infimum of Complete Uniform Spaces under Hausdorff Condition

Informal description

Let $X$ be a type and $(u_i)_{i \in \iota}$ be a family of uniform space structures on $X$ such that: 1. Each uniform space $(X, u_i)$ is complete. 2. There exists a Hausdorff topological space structure $t$ on $X$ that is finer than all the topological spaces induced by the $u_i$. Then the infimum uniform space $\bigsqcap_{i \in \iota} u_i$ is also complete on $X$.