English
If hf is uniformly continuous on uncurry f, then the 2-ary extension applied to (ι a, ι' b) equals f a b.
Русский
Если hf равномерно непрерывно на uncurry f, то расширение₂ на (ι a, ι' b) равно f a b.
LaTeX
$$$ (hf: UniformContinuous (uncurry f)) \to (a: \alpha) (b: \beta), \ pkg.extend₂ pkg' f (ι a) (ι' b) = f a b $$$
Lean4
/-- Let `X` be a compact topological space, `α` a uniform space, and `F : ι → (X → α)` an
equicontinuous family. Then, the uniform structures of uniform convergence and pointwise
convergence induce the same uniform structure on `ι`.
In other words, pointwise convergence and uniform convergence coincide on an equicontinuous
subset of `X → α`.
Consider using `Equicontinuous.isUniformInducing_uniformFun_iff_pi` and
`Equicontinuous.inducing_uniformFun_iff_pi` instead, to avoid rewriting instances. -/
theorem comap_uniformFun_eq [CompactSpace X] (F_eqcont : Equicontinuous F) :
(UniformFun.uniformSpace X α).comap F = (Pi.uniformSpace _).comap F := by
-- The `≤` inequality is trivial
refine
le_antisymm (UniformSpace.comap_mono UniformFun.uniformContinuous_toFun)
?_
-- A bit of rewriting to get a nice intermediate statement.
simp_rw [UniformSpace.comap, UniformSpace.le_def, uniformity_comap, Pi.uniformity, Filter.comap_iInf, comap_comap,
Function.comp_def]
refine
((UniformFun.hasBasis_uniformity X α).comap (Prod.map F F)).ge_iff.mpr
?_
-- Core of the proof: we need to show that, for any entourage `U` in `α`,
-- the set `𝐓(U) := {(i,j) : ι × ι | ∀ x : X, (F i x, F j x) ∈ U}` belongs to the filter
-- `⨅ x, comap ((i,j) ↦ (F i x, F j x)) (𝓤 α)`.
-- In other words, we have to show that it contains a finite intersection of
-- sets of the form `𝐒(V, x) := {(i,j) : ι × ι | (F i x, F j x) ∈ V}` for some
-- `x : X` and `V ∈ 𝓤 α`.
intro U hU
rcases comp_comp_symm_mem_uniformity_sets hU with
⟨V, hV, Vsymm, hVU⟩
-- Set `Ω x := {y | ∀ i, (F i x, F i y) ∈ V}`. The equicontinuity of `F` guarantees that
-- each `Ω x` is a neighborhood of `x`.
let Ω x : Set X :=
{y | ∀ i, (F i x, F i y) ∈ V}
-- Hence, by compactness of `X`, we can find some `A ⊆ X` finite such that the `Ω a`s for `a ∈ A`
-- still cover `X`.
rcases CompactSpace.elim_nhds_subcover Ω (fun x ↦ F_eqcont x V hV) with
⟨A, Acover⟩
-- We now claim that `⋂ a ∈ A, 𝐒(V, a) ⊆ 𝐓(U)`.
have : (⋂ a ∈ A, {ij : ι × ι | (F ij.1 a, F ij.2 a) ∈ V}) ⊆ (Prod.map F F) ⁻¹' UniformFun.gen X α U := by
-- Given `(i, j) ∈ ⋂ a ∈ A, 𝐒(V, a)` and `x : X`, we have to prove that `(F i x, F j x) ∈ U`.
rintro ⟨i, j⟩ hij x
rw [mem_iInter₂] at hij
rcases mem_iUnion₂.mp (Acover.symm.subset <| mem_univ x) with
⟨a, ha, hax⟩
-- Since `(i, j) ∈ 𝐒(V, a)` we also have `(F i a, F j a) ∈ V`, and finally we get
-- `(F i x, F j x) ∈ V ○ V ○ V ⊆ U`.
exact
hVU
(prodMk_mem_compRel (prodMk_mem_compRel (Vsymm.mk_mem_comm.mp (hax i)) (hij a ha)) (hax j))
-- This completes the proof.
exact mem_of_superset (A.iInter_mem_sets.mpr fun x _ ↦ mem_iInf_of_mem x <| preimage_mem_comap hV) this
