English
If g is a UniformEmbedding, then precomposition by g induces a UniformEmbedding on the function spaces: f ↦ f ∘ g.
Русский
Если g является UniformEmbedding, то отображение f ↦ f∘g является UniformEmbedding на пространствах функций.
LaTeX
$$$\text{IsUniformEmbedding } g \Rightarrow \text{IsUniformEmbedding}(f \mapsto f \circ g)$$$
Lean4
theorem uniformSpace_eq_iInf_precomp_of_cover {δ : ι → Type*} [∀ i, TopologicalSpace (δ i)] (φ : Π i, C(δ i, α))
(h_proper : ∀ i, IsProperMap (φ i)) (h_lf : LocallyFinite fun i ↦ range (φ i)) (h_cover : ⋃ i, range (φ i) = univ) :
(inferInstanceAs <| UniformSpace C(α, β)) = ⨅ i, .comap (comp · (φ i)) inferInstance := by
-- We check the analogous result for `UniformOnFun` using
-- `UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover`...
set 𝔖 : Set (Set α) := {K | IsCompact K}
set 𝔗 : Π i, Set (Set (δ i)) := fun i ↦ {K | IsCompact K}
have h_image : ∀ i, MapsTo (φ i '' ·) (𝔗 i) 𝔖 := fun i K hK ↦ hK.image (φ i).continuous
have h_preimage : ∀ i, MapsTo (φ i ⁻¹' ·) 𝔖 (𝔗 i) := fun i K ↦ (h_proper i).isCompact_preimage
have h_cover' : ∀ S ∈ 𝔖, ∃ I : Set ι, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i) := fun S hS ↦
by
refine ⟨{i | (range (φ i) ∩ S).Nonempty}, h_lf.finite_nonempty_inter_compact hS, inter_eq_right.mp ?_⟩
simp_rw [iUnion₂_inter, mem_setOf, iUnion_nonempty_self, ← iUnion_inter, h_cover, univ_inter]
-- ... and we just pull it back.
simp_rw +zetaDelta [compactConvergenceUniformSpace, replaceTopology_eq,
UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover _ _ _ h_image h_preimage h_cover', UniformSpace.comap_iInf, ←
UniformSpace.comap_comap]
rfl
