English
There is a natural uniform equivalence between C(α,β) and C(γ,δ) induced by a homeomorphism α ≃ₜ γ and a uniform equivalence β ≃ᵤ δ.
Русский
Существует естественное униформное эквивалентное отображение между пространствами C(α,β) и C(γ,δ), порожденное гомеоморфизмом α ≃ₜ γ и униформным эквивалентом β ≃ᵤ δ.
LaTeX
$$$\varphi : α \simeq_t γ$, $\psi : β \simeq_u δ$ ⟹ $C(α, β) \simeq_u C(γ, δ)$, с формулами предобраза и образа$$
Lean4
theorem uniformSpace_eq_inf_precomp_of_cover {δ₁ δ₂ : Type*} [TopologicalSpace δ₁] [TopologicalSpace δ₂] (φ₁ : C(δ₁, α))
(φ₂ : C(δ₂, α)) (h_proper₁ : IsProperMap φ₁) (h_proper₂ : IsProperMap φ₂) (h_cover : range φ₁ ∪ range φ₂ = univ) :
(inferInstanceAs <| UniformSpace C(α, β)) = .comap (comp · φ₁) inferInstance ⊓ .comap (comp · φ₂) inferInstance :=
by
-- We check the analogous result for `UniformOnFun` using
-- `UniformOnFun.uniformSpace_eq_inf_precomp_of_cover`...
set 𝔖 : Set (Set α) := {K | IsCompact K}
set 𝔗₁ : Set (Set δ₁) := {K | IsCompact K}
set 𝔗₂ : Set (Set δ₂) := {K | IsCompact K}
have h_image₁ : MapsTo (φ₁ '' ·) 𝔗₁ 𝔖 := fun K hK ↦ hK.image φ₁.continuous
have h_image₂ : MapsTo (φ₂ '' ·) 𝔗₂ 𝔖 := fun K hK ↦ hK.image φ₂.continuous
have h_preimage₁ : MapsTo (φ₁ ⁻¹' ·) 𝔖 𝔗₁ := fun K ↦ h_proper₁.isCompact_preimage
have h_preimage₂ : MapsTo (φ₂ ⁻¹' ·) 𝔖 𝔗₂ := fun K ↦ h_proper₂.isCompact_preimage
have h_cover' : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂ := fun S _ ↦
h_cover ▸
subset_univ
_
-- ... and we just pull it back.
simp_rw +zetaDelta [compactConvergenceUniformSpace, replaceTopology_eq,
UniformOnFun.uniformSpace_eq_inf_precomp_of_cover _ _ _ _ _ h_image₁ h_image₂ h_preimage₁ h_preimage₂ h_cover',
UniformSpace.comap_inf, ← UniformSpace.comap_comap]
rfl
