Topology and uniform structure of uniform convergence #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This files endows α → β with the topologies / uniform structures of
- uniform convergence on
α - uniform convergence on a specified family
𝔖of sets ofα, also called𝔖-convergence
Since α → β is already endowed with the topologies and uniform structures of pointwise
convergence, we introduce type aliases uniform_fun α β (denoted α →ᵤ β) and
uniform_on_fun α β 𝔖 (denoted α →ᵤ[𝔖] β) and we actually endow these with the structures
of uniform and 𝔖-convergence respectively.
Usual examples of the second construction include :
- the topology of compact convergence, when
𝔖is the set of compacts ofα - the strong topology on the dual of a topological vector space (TVS)
E, when𝔖is the set of Von Neuman bounded subsets ofE - the weak-* topology on the dual of a TVS
E, when𝔖is the set of singletons ofE.
This file contains a lot of technical facts, so it is heavily commented, proofs included!
Main definitions #
uniform_fun.gen: basis sets for the uniformity of uniform convergence. These are sets of the formS(V) := {(f, g) | ∀ x : α, (f x, g x) ∈ V}for someV : set (β × β)uniform_fun.uniform_space: uniform structure of uniform convergence. This is theuniform_spaceonα →ᵤ βwhose uniformity is generated by the setsS(V)forV ∈ 𝓤 β. We will denote this uniform space as𝒰(α, β, uβ), both in the comments and as a local notation in the Lean code, whereuβis the uniform space structure onβ. This is declared as an instance onα →ᵤ β.uniform_on_fun.uniform_space: uniform structure of𝔖-convergence, where𝔖 : set (set α). This is the infimum, forS ∈ 𝔖, of the pullback of𝒰 S βby the map of restriction toS. We will denote it𝒱(α, β, 𝔖, uβ), whereuβis the uniform space structure onβ. This is declared as an instance onα →ᵤ[𝔖] β.
Main statements #
Basic properties #
uniform_fun.uniform_continuous_eval: evaluation is uniformly continuous onα →ᵤ β.uniform_fun.t2_space: the topology of uniform convergence onα →ᵤ βis T₂ ifβis T₂.uniform_fun.tendsto_iff_tendsto_uniformly:𝒰(α, β, uβ)is indeed the uniform structure of uniform convergenceuniform_on_fun.uniform_continuous_eval_of_mem: evaluation at a point contained in a set of𝔖is uniformly continuous onα →ᵤ[𝔖] βuniform_on_fun.t2_space_of_covering: the topology of𝔖-convergence onα →ᵤ[𝔖] βis T₂ ifβis T₂ and𝔖coversαuniform_on_fun.tendsto_iff_tendsto_uniformly_on:𝒱(α, β, 𝔖 uβ)is indeed the uniform structure of𝔖-convergence
Functoriality and compatibility with product of uniform spaces #
In order to avoid the need for filter bases as much as possible when using these definitions,
we develop an extensive API for manipulating these structures abstractly. As usual in the topology
section of mathlib, we first state results about the complete lattices of uniform_spaces on
fixed types, and then we use these to deduce categorical-like results about maps between two
uniform spaces.
We only describe these in the harder case of 𝔖-convergence, as the names of the corresponding
results for uniform convergence can easily be guessed.
Order statements #
uniform_on_fun.mono: letu₁,u₂be two uniform structures onγand𝔖₁ 𝔖₂ : set (set α). Ifu₁ ≤ u₂and𝔖₂ ⊆ 𝔖₁then𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂).uniform_on_fun.infi_eq: ifuis a family of uniform structures onγ, then𝒱(α, γ, 𝔖, (⨅ i, u i)) = ⨅ i, 𝒱(α, γ, 𝔖, u i).uniform_on_fun.comap_eq: ifuis a uniform structures onβandf : γ → β, then𝒱(α, γ, 𝔖, comap f u) = comap (λ g, f ∘ g) 𝒱(α, γ, 𝔖, u₁).
An interesting note about these statements is that they are proved without ever unfolding the basis
definition of the uniform structure of uniform convergence! Instead, we build a
(not very interesting) Galois connection uniform_convergence.gc and then rely on the Galois
connection API to do most of the work.
Morphism statements (unbundled) #
uniform_on_fun.postcomp_uniform_continuous: iff : γ → βis uniformly continuous, then(λ g, f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β)is uniformly continuous.uniform_on_fun.postcomp_uniform_inducing: iff : γ → βis a uniform inducing, then(λ g, f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β)is a uniform inducing.uniform_on_fun.precomp_uniform_continuous: letf : γ → α,𝔖 : set (set α),𝔗 : set (set γ), and assume that∀ T ∈ 𝔗, f '' T ∈ 𝔖. Then, the function(λ g, g ∘ f) : (α →ᵤ[𝔖] β) → (γ →ᵤ[𝔗] β)is uniformly continuous.
Isomorphism statements (bundled) #
uniform_on_fun.congr_right: turn a uniform isomorphismγ ≃ᵤ βinto a uniform isomorphism(α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β)by post-composing.uniform_on_fun.congr_left: turn a bijectione : γ ≃ αsuch that we have both∀ T ∈ 𝔗, e '' T ∈ 𝔖and∀ S ∈ 𝔖, e ⁻¹' S ∈ 𝔗into a uniform isomorphism(γ →ᵤ[𝔗] β) ≃ᵤ (α →ᵤ[𝔖] β)by pre-composing.uniform_on_fun.uniform_equiv_Pi_comm: the natural bijection betweenα → Π i, δ iandΠ i, α → δ i, upgraded to a uniform isomorphism betweenα →ᵤ[𝔖] (Π i, δ i)andΠ i, α →ᵤ[𝔖] δ i.
Important use cases #
- If
Gis a uniform group, thenα →ᵤ[𝔖] Gis a uniform group: since(/) : G × G → Gis uniformly continuous,uniform_convergence_on.postcomp_uniform_continuoustells us that((/) ∘ —) : (α →ᵤ[𝔖] G × G) → (α →ᵤ[𝔖] G)is uniformly continuous. By precomposing withuniform_convergence_on.uniform_equiv_prod_arrow, this gives that(/) : (α →ᵤ[𝔖] G) × (α →ᵤ[𝔖] G) → (α →ᵤ[𝔖] G)is also uniformly continuous - The transpose of a continuous linear map is continuous for the strong topologies: since
continuous linear maps are uniformly continuous and map bounded sets to bounded sets,
this is just a special case of
uniform_convergence_on.precomp_uniform_continuous.
TODO #
- Show that the uniform structure of
𝔖-convergence is exactly the structure of𝔖'-convergence, where𝔖'is the noncovering bornology (i.e not whatbornologycurrently refers to in mathlib) generated by𝔖.
References #
Tags #
uniform convergence
The type of functions from α to β equipped with the uniform structure and topology of
uniform convergence. We denote it α →ᵤ β.
Equations
- uniform_fun α β = (α → β)
Instances for uniform_fun
- uniform_fun.nonempty
- uniform_fun.uniform_space
- uniform_fun.topological_space
- uniform_fun.t2_space
- uniform_fun.monoid
- uniform_fun.add_monoid
- uniform_fun.comm_monoid
- uniform_fun.add_comm_monoid
- uniform_fun.group
- uniform_fun.add_group
- uniform_fun.comm_group
- uniform_fun.add_comm_group
- uniform_fun.module
- uniform_fun.uniform_group
- uniform_fun.uniform_add_group
The type of functions from α to β equipped with the uniform structure and topology of
uniform convergence on some family 𝔖 of subsets of α. We denote it α →ᵤ[𝔖] β.
Equations
- uniform_on_fun α β 𝔖 = (α → β)
Instances for uniform_on_fun
- uniform_on_fun.nonempty
- uniform_on_fun.uniform_space
- uniform_on_fun.topological_space
- uniform_on_fun.monoid
- uniform_on_fun.add_monoid
- uniform_on_fun.comm_monoid
- uniform_on_fun.add_comm_monoid
- uniform_on_fun.group
- uniform_on_fun.add_group
- uniform_on_fun.comm_group
- uniform_on_fun.add_comm_group
- uniform_on_fun.module
- uniform_on_fun.uniform_group
- uniform_on_fun.uniform_add_group
Reinterpret f : α → β as an element of α →ᵤ β.
Equations
- uniform_fun.of_fun = {to_fun := λ (x : α → β), x, inv_fun := λ (x : uniform_fun α β), x, left_inv := _, right_inv := _}
Reinterpret f : α → β as an element of α →ᵤ[𝔖] β.
Equations
- uniform_on_fun.of_fun 𝔖 = {to_fun := λ (x : α → β), x, inv_fun := λ (x : uniform_on_fun α β 𝔖), x, left_inv := _, right_inv := _}
Reinterpret f : α →ᵤ β as an element of α → β.
Equations
Reinterpret f : α →ᵤ[𝔖] β as an element of α → β.
Equations
Basis sets for the uniformity of uniform convergence: gen α β V is the set of pairs (f, g)
of functions α →ᵤ β such that ∀ x, (f x, g x) ∈ V.
Equations
- uniform_fun.gen α β V = {uv : uniform_fun α β × uniform_fun α β | ∀ (x : α), (uv.fst x, uv.snd x) ∈ V}
If 𝓕 is a filter on β × β, then the set of all uniform_convergence.gen α β V for
V ∈ 𝓕 is a filter basis on (α →ᵤ β) × (α →ᵤ β). This will only be applied to 𝓕 = 𝓤 β when
β is equipped with a uniform_space structure, but it is useful to define it for any filter in
order to be able to state that it has a lower adjoint (see uniform_convergence.gc).
For 𝓕 : filter (β × β), this is the set of all uniform_convergence.gen α β V for
V ∈ 𝓕 as a bundled filter_basis over (α →ᵤ β) × (α →ᵤ β). This will only be applied to
𝓕 = 𝓤 β when β is equipped with a uniform_space structure, but it is useful to define it for
any filter in order to be able to state that it has a lower adjoint
(see uniform_convergence.gc).
Equations
- uniform_fun.basis α β 𝓕 = _.filter_basis
For 𝓕 : filter (β × β), this is the filter generated by the filter basis
uniform_convergence.basis α β 𝓕. For 𝓕 = 𝓤 β, this will be the uniformity of uniform
convergence on α.
Equations
- uniform_fun.filter α β 𝓕 = (uniform_fun.basis α β 𝓕).filter
The function uniform_convergence.filter α β : filter (β × β) → filter ((α →ᵤ β) × (α →ᵤ β))
has a lower adjoint l (in the sense of galois_connection). The exact definition of l is not
interesting; we will only use that it exists (in uniform_convergence.mono and
uniform_convergence.infi_eq) and that
l (filter.map (prod.map f f) 𝓕) = filter.map (prod.map ((∘) f) ((∘) f)) (l 𝓕) for each
𝓕 : filter (γ × γ) and f : γ → α (in uniform_convergence.comap_eq).
Core of the uniform structure of uniform convergence.
Equations
- uniform_fun.uniform_core α β = uniform_space.core.mk_of_basis (uniform_fun.basis α β (uniformity β)) _ _ _
Uniform structure of uniform convergence, declared as an instance on α →ᵤ β.
We will denote it 𝒰(α, β, uβ) in the rest of this file.
Equations
Topology of uniform convergence, declared as an instance on α →ᵤ β.
Equations
By definition, the uniformity of α →ᵤ β admits the family {(f, g) | ∀ x, (f x, g x) ∈ V}
for V ∈ 𝓤 β as a filter basis.
The uniformity of α →ᵤ β admits the family {(f, g) | ∀ x, (f x, g x) ∈ V} for V ∈ 𝓑 as
a filter basis, for any basis 𝓑 of 𝓤 β (in the case 𝓑 = (𝓤 β).as_basis this is true by
definition).
For f : α →ᵤ β, 𝓝 f admits the family {g | ∀ x, (f x, g x) ∈ V} for V ∈ 𝓑 as a filter
basis, for any basis 𝓑 of 𝓤 β.
For f : α →ᵤ β, 𝓝 f admits the family {g | ∀ x, (f x, g x) ∈ V} for V ∈ 𝓤 β as a
filter basis.
Evaluation at a fixed point is uniformly continuous on α →ᵤ β.
If u₁ and u₂ are two uniform structures on γ and u₁ ≤ u₂, then
𝒰(α, γ, u₁) ≤ 𝒰(α, γ, u₂).
If u is a family of uniform structures on γ, then
𝒰(α, γ, (⨅ i, u i)) = ⨅ i, 𝒰(α, γ, u i).
If u₁ and u₂ are two uniform structures on γ, then
𝒰(α, γ, u₁ ⊓ u₂) = 𝒰(α, γ, u₁) ⊓ 𝒰(α, γ, u₂).
If u is a uniform structures on β and f : γ → β, then
𝒰(α, γ, comap f u) = comap (λ g, f ∘ g) 𝒰(α, γ, u₁).
Post-composition by a uniformly continuous function is uniformly continuous on α →ᵤ β.
More precisely, if f : γ → β is uniformly continuous, then (λ g, f ∘ g) : (α →ᵤ γ) → (α →ᵤ β)
is uniformly continuous.
Post-composition by a uniform inducing is a uniform inducing for the uniform structures of uniform convergence.
More precisely, if f : γ → β is a uniform inducing, then (λ g, f ∘ g) : (α →ᵤ γ) → (α →ᵤ β) is
a uniform inducing.
Turn a uniform isomorphism γ ≃ᵤ β into a uniform isomorphism (α →ᵤ γ) ≃ᵤ (α →ᵤ β) by
post-composing.
Equations
- uniform_fun.congr_right e = {to_equiv := {to_fun := (equiv.Pi_congr_right (λ (a : α), e.to_equiv)).to_fun, inv_fun := (equiv.Pi_congr_right (λ (a : α), e.to_equiv)).inv_fun, left_inv := _, right_inv := _}, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}
Pre-composition by a any function is uniformly continuous for the uniform structures of uniform convergence.
More precisely, for any f : γ → α, the function (λ g, g ∘ f) : (α →ᵤ β) → (γ →ᵤ β) is uniformly
continuous.
Turn a bijection γ ≃ α into a uniform isomorphism
(γ →ᵤ β) ≃ᵤ (α →ᵤ β) by pre-composing.
Equations
- uniform_fun.congr_left e = {to_equiv := {to_fun := (e.arrow_congr (equiv.refl β)).to_fun, inv_fun := (e.arrow_congr (equiv.refl β)).inv_fun, left_inv := _, right_inv := _}, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}
The topology of uniform convergence is T₂.
The natural map uniform_fun.to_fun from α →ᵤ β to α → β is uniformly continuous.
In other words, the uniform structure of uniform convergence is finer than that of pointwise convergence, aka the product uniform structure.
The topology of uniform convergence indeed gives the same notion of convergence as
tendsto_uniformly.
The natural bijection between α → β × γ and (α → β) × (α → γ), upgraded to a uniform
isomorphism between α →ᵤ β × γ and (α →ᵤ β) × (α →ᵤ γ).
Equations
- uniform_fun.uniform_equiv_prod_arrow = (equiv.arrow_prod_equiv_prod_arrow β γ α).to_uniform_equiv_of_uniform_inducing uniform_fun.uniform_equiv_prod_arrow._proof_1
The natural bijection between α → Π i, δ i and Π i, α → δ i, upgraded to a uniform
isomorphism between α →ᵤ (Π i, δ i) and Π i, α →ᵤ δ i.
Equations
- uniform_fun.uniform_equiv_Pi_comm α δ = (equiv.Pi_comm (λ (ᾰ : α) (i : ι), δ i)).to_uniform_equiv_of_uniform_inducing _
Basis sets for the uniformity of 𝔖-convergence: for S : set α and V : set (β × β),
gen 𝔖 S V is the set of pairs (f, g) of functions α →ᵤ[𝔖] β such that
∀ x ∈ S, (f x, g x) ∈ V. Note that the family 𝔖 : set (set α) is only used to specify which
type alias of α → β to use here.
Equations
- uniform_on_fun.gen 𝔖 S V = {uv : uniform_on_fun α β 𝔖 × uniform_on_fun α β 𝔖 | ∀ (x : α), x ∈ S → (uv.fst x, uv.snd x) ∈ V}
For S : set α and V : set (β × β), we have
uniform_on_fun.gen 𝔖 S V = (S.restrict × S.restrict) ⁻¹' (uniform_fun.gen S β V).
This is the crucial fact for proving that the family uniform_on_fun.gen S V for S ∈ 𝔖 and
V ∈ 𝓤 β is indeed a basis for the uniformity α →ᵤ[𝔖] β endowed with 𝒱(α, β, 𝔖, uβ)
the uniform structure of 𝔖-convergence, as defined in uniform_on_fun.uniform_space.
uniform_on_fun.gen is antitone in the first argument and monotone in the second.
If 𝔖 : set (set α) is nonempty and directed and 𝓑 is a filter basis on β × β, then the
family uniform_on_fun.gen 𝔖 S V for S ∈ 𝔖 and V ∈ 𝓑 is a filter basis on
(α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β).
We will show in has_basis_uniformity_of_basis that, if 𝓑 is a basis for 𝓤 β, then the
corresponding filter is the uniformity of α →ᵤ[𝔖] β.
Uniform structure of 𝔖-convergence, i.e uniform convergence on the elements of 𝔖,
declared as an instance on α →ᵤ[𝔖] β. It is defined as the infimum, for S ∈ 𝔖, of the pullback
by S.restrict, the map of restriction to S, of the uniform structure 𝒰(s, β, uβ) on
↥S →ᵤ β. We will denote it 𝒱(α, β, 𝔖, uβ), where uβ is the uniform structure on β.
Equations
- uniform_on_fun.uniform_space α β 𝔖 = ⨅ (s : set α) (hs : s ∈ 𝔖), uniform_space.comap s.restrict (uniform_fun.uniform_space ↥s β)
Topology of 𝔖-convergence, i.e uniform convergence on the elements of 𝔖, declared as an
instance on α →ᵤ[𝔖] β.
Equations
The topology of 𝔖-convergence is the infimum, for S ∈ 𝔖, of topology induced by the map
of S.restrict : (α →ᵤ[𝔖] β) → (↥S →ᵤ β) of restriction to S, where ↥S →ᵤ β is endowed with
the topology of uniform convergence.
If 𝔖 : set (set α) is nonempty and directed and 𝓑 is a filter basis of 𝓤 β, then the
uniformity of α →ᵤ[𝔖] β admits the family {(f, g) | ∀ x ∈ S, (f x, g x) ∈ V} for S ∈ 𝔖 and
V ∈ 𝓑 as a filter basis.
If 𝔖 : set (set α) is nonempty and directed, then the uniformity of α →ᵤ[𝔖] β admits the
family {(f, g) | ∀ x ∈ S, (f x, g x) ∈ V} for S ∈ 𝔖 and V ∈ 𝓤 β as a filter basis.
For f : α →ᵤ[𝔖] β, where 𝔖 : set (set α) is nonempty and directed, 𝓝 f admits the
family {g | ∀ x ∈ S, (f x, g x) ∈ V} for S ∈ 𝔖 and V ∈ 𝓑 as a filter basis, for any basis
𝓑 of 𝓤 β.
For f : α →ᵤ[𝔖] β, where 𝔖 : set (set α) is nonempty and directed, 𝓝 f admits the
family {g | ∀ x ∈ S, (f x, g x) ∈ V} for S ∈ 𝔖 and V ∈ 𝓤 β as a filter basis.
If S ∈ 𝔖, then the restriction to S is a uniformly continuous map from α →ᵤ[𝔖] β to
↥S →ᵤ β.
Let u₁, u₂ be two uniform structures on γ and 𝔖₁ 𝔖₂ : set (set α). If u₁ ≤ u₂ and
𝔖₂ ⊆ 𝔖₁ then 𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂).
If x : α is in some S ∈ 𝔖, then evaluation at x is uniformly continuous on
α →ᵤ[𝔖] β.
If u is a family of uniform structures on γ, then
𝒱(α, γ, 𝔖, (⨅ i, u i)) = ⨅ i, 𝒱(α, γ, 𝔖, u i).
If u₁ and u₂ are two uniform structures on γ, then
𝒱(α, γ, 𝔖, u₁ ⊓ u₂) = 𝒱(α, γ, 𝔖, u₁) ⊓ 𝒱(α, γ, 𝔖, u₂).
If u is a uniform structures on β and f : γ → β, then
𝒱(α, γ, 𝔖, comap f u) = comap (λ g, f ∘ g) 𝒱(α, γ, 𝔖, u₁).
Post-composition by a uniformly continuous function is uniformly continuous for the
uniform structures of 𝔖-convergence.
More precisely, if f : γ → β is uniformly continuous, then
(λ g, f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β) is uniformly continuous.
Post-composition by a uniform inducing is a uniform inducing for the
uniform structures of 𝔖-convergence.
More precisely, if f : γ → β is a uniform inducing, then
(λ g, f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β) is a uniform inducing.
Turn a uniform isomorphism γ ≃ᵤ β into a uniform isomorphism (α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β)
by post-composing.
Equations
- uniform_on_fun.congr_right e = {to_equiv := {to_fun := (equiv.Pi_congr_right (λ (a : α), e.to_equiv)).to_fun, inv_fun := (equiv.Pi_congr_right (λ (a : α), e.to_equiv)).inv_fun, left_inv := _, right_inv := _}, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}
Let f : γ → α, 𝔖 : set (set α), 𝔗 : set (set γ), and assume that ∀ T ∈ 𝔗, f '' T ∈ 𝔖.
Then, the function (λ g, g ∘ f) : (α →ᵤ[𝔖] β) → (γ →ᵤ[𝔗] β) is uniformly continuous.
Note that one can easily see that assuming ∀ T ∈ 𝔗, ∃ S ∈ 𝔖, f '' T ⊆ S would work too, but
we will get this for free when we prove that 𝒱(α, β, 𝔖, uβ) = 𝒱(α, β, 𝔖', uβ) where 𝔖' is the
noncovering bornology generated by 𝔖.
Turn a bijection e : γ ≃ α such that we have both ∀ T ∈ 𝔗, e '' T ∈ 𝔖 and
∀ S ∈ 𝔖, e ⁻¹' S ∈ 𝔗 into a uniform isomorphism (γ →ᵤ[𝔗] β) ≃ᵤ (α →ᵤ[𝔖] β) by pre-composing.
Equations
- uniform_on_fun.congr_left e he he' = {to_equiv := {to_fun := (e.arrow_congr (equiv.refl β)).to_fun, inv_fun := (e.arrow_congr (equiv.refl β)).inv_fun, left_inv := _, right_inv := _}, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}
If 𝔖 covers α, then the topology of 𝔖-convergence is T₂.
If 𝔖 covers α, the natural map uniform_on_fun.to_fun from α →ᵤ[𝔖] β to α → β is
uniformly continuous.
In other words, if 𝔖 covers α, then the uniform structure of 𝔖-convergence is finer than
that of pointwise convergence.
Convergence in the topology of 𝔖-convergence means uniform convergence on S (in the sense
of tendsto_uniformly_on) for all S ∈ 𝔖.
The natural bijection between α → β × γ and (α → β) × (α → γ), upgraded to a uniform
isomorphism between α →ᵤ[𝔖] β × γ and (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ).
Equations
- uniform_on_fun.uniform_equiv_prod_arrow = ((uniform_on_fun.of_fun 𝔖).symm.trans ((equiv.arrow_prod_equiv_prod_arrow β γ α).trans ((uniform_on_fun.of_fun 𝔖).prod_congr (uniform_on_fun.of_fun 𝔖)))).to_uniform_equiv_of_uniform_inducing uniform_on_fun.uniform_equiv_prod_arrow._proof_1
The natural bijection between α → Π i, δ i and Π i, α → δ i, upgraded to a uniform
isomorphism between α →ᵤ[𝔖] (Π i, δ i) and Π i, α →ᵤ[𝔖] δ i.
Equations
- uniform_on_fun.uniform_equiv_Pi_comm 𝔖 δ = (equiv.Pi_comm (λ (ᾰ : α) (i : ι), δ i)).to_uniform_equiv_of_uniform_inducing _