English
A uniform isomorphism between γ and β yields a uniform isomorphism between the corresponding 𝔖-convergence spaces by postcomposition; the proof constructs the uniform isomorphism.
Русский
Равномерная изоморфизм между γ и β даёт равномерный изоморфизм между соответствующими 𝔖-конвергенциями путём пост-композиции; доказательство конструирует равномерный изоморфизм.
LaTeX
$$UniformOnFun.congrRight {e : γ ≃ᵤ β} : (α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β).$$
Lean4
/-- If each point of `α` admits a neighbourhood `V ∈ 𝔖`,
then the evaluation of `f : α →ᵤ[𝔖] β` at `x : α` is continuous in `(f, x)`
on the set of `(f, x)` such that `f` is continuous at `x`. -/
protected theorem continuousOn_eval₂ [TopologicalSpace α] (h𝔖 : ∀ x, ∃ V ∈ 𝔖, V ∈ 𝓝 x) :
ContinuousOn (fun fx : (α →ᵤ[𝔖] β) × α ↦ toFun 𝔖 fx.1 fx.2) {fx | ContinuousAt (toFun 𝔖 fx.1) fx.2} :=
fun (_f, x) hc ↦ (UniformOnFun.continuousAt_eval₂ (h𝔖 x) hc).continuousWithinAt
