English
The extension ψ is uniformly continuous given uniform inducing, dense range, and a uniformly continuous f.
Русский
Расширение ψ является равномерно непрерывным при условиях: равномерно индуцирующее, плотный образ и равномерная непрерывность f.
LaTeX
$$$\text{Uniformly extend }\psi\text{ is uniformly continuous under the hypotheses.}$$$
Lean4
theorem uniformContinuous_uniformly_extend [CompleteSpace γ] : UniformContinuous ψ := fun d hd =>
let ⟨s, hs, hs_comp⟩ := comp3_mem_uniformity hd
have h_pnt : ∀ {a m}, m ∈ 𝓝 a → ∃ c ∈ f '' (e ⁻¹' m), (c, ψ a) ∈ s ∧ (ψ a, c) ∈ s := fun {a m} hm =>
have nb : NeBot (map f (comap e (𝓝 a))) := ((h_e.isDenseInducing h_dense).comap_nhds_neBot _).map _
have : f '' (e ⁻¹' m) ∩ ({c | (c, ψ a) ∈ s} ∩ {c | (ψ a, c) ∈ s}) ∈ map f (comap e (𝓝 a)) :=
inter_mem (image_mem_map <| preimage_mem_comap <| hm)
(uniformly_extend_spec h_e h_dense h_f _ (inter_mem (mem_nhds_right _ hs) (mem_nhds_left _ hs)))
nb.nonempty_of_mem this
have : (Prod.map f f) ⁻¹' s ∈ 𝓤 β := h_f hs
have : (Prod.map f f) ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α) := by rwa [← h_e.comap_uniformity] at this
let ⟨t, ht, ts⟩ := this
show (Prod.map ψ ψ) ⁻¹' d ∈ 𝓤 α from
mem_of_superset (interior_mem_uniformity ht) fun ⟨x₁, x₂⟩ hx_t =>
by
have : interior t ∈ 𝓝 (x₁, x₂) := isOpen_interior.mem_nhds hx_t
let ⟨m₁, hm₁, m₂, hm₂, (hm : m₁ ×ˢ m₂ ⊆ interior t)⟩ := mem_nhds_prod_iff.mp this
obtain ⟨_, ⟨a, ha₁, rfl⟩, _, ha₂⟩ := h_pnt hm₁
obtain ⟨_, ⟨b, hb₁, rfl⟩, hb₂, _⟩ := h_pnt hm₂
have : Prod.map f f (a, b) ∈ s := ts <| mem_preimage.2 <| interior_subset (@hm (e a, e b) ⟨ha₁, hb₁⟩)
exact hs_comp ⟨f a, ha₂, ⟨f b, this, hb₂⟩⟩
