English
If f is a uniform embedding, then the postcomposition map is a uniform embedding between the corresponding 𝔖-convergence spaces.
Русский
Если f — равномерное вложение, то отображение по пост-композиции является равномерным вложением между 𝔖-конвергенциями.
LaTeX
$$IsUniformEmbedding f → IsUniformEmbedding (Function.comp (UniformOnFun.ofFun 𝔖) (Function.comp (fun x => Function.comp f x) (UniformOnFun.toFun 𝔖))).$$
Lean4
/-- If `f : α →ᵤ[𝔖] β` is continuous at `x` and `x` admits a neighbourhood `V ∈ 𝔖`,
then evaluation of `g : α →ᵤ[𝔖] β` at `y : α` is continuous in `(g, y)` at `(f, x)`. -/
protected theorem continuousAt_eval₂ [TopologicalSpace α] {f : α →ᵤ[𝔖] β} {x : α} (h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x)
(hc : ContinuousAt (toFun 𝔖 f) x) : ContinuousAt (fun fx : (α →ᵤ[𝔖] β) × α ↦ toFun 𝔖 fx.1 fx.2) (f, x) :=
by
rw [ContinuousAt, nhds_eq_comap_uniformity, tendsto_comap_iff, ← lift'_comp_uniformity, tendsto_lift']
intro U hU
rcases h𝔖 with ⟨V, hV, hVx⟩
filter_upwards [prod_mem_nhds (UniformOnFun.gen_mem_nhds _ _ _ hV hU)
(inter_mem hVx <| hc <| UniformSpace.ball_mem_nhds _ hU)] with
⟨g, y⟩ ⟨hg, hyV, hy⟩ using ⟨toFun 𝔖 f y, hy, hg y hyV⟩
