English
Evaluation at a fixed point x ∈ α is uniformly continuous on α →ᵤ β; i.e., the map f ↦ f(x) is uniformly continuous.
Русский
Оценка в фиксированной точке x является равномерно непрерывной на α →ᵤ β; т.е. f ↦ f(x) равномерно непрерывна.
LaTeX
$$$$ \text{eval}_x: (α \to^{u} β) \to β \quad \text{is uniformly continuous for each } x \in α.$$$$
Lean4
/-- Evaluation at a fixed point is uniformly continuous on `α →ᵤ β`. -/
theorem uniformContinuous_eval (x : α) : UniformContinuous (Function.eval x ∘ toFun : (α →ᵤ β) → β) :=
by
change _ ≤ _
rw [map_le_iff_le_comap, (UniformFun.hasBasis_uniformity α β).le_basis_iff ((𝓤 _).basis_sets.comap _)]
exact fun U hU => ⟨U, hU, fun uv huv => huv x⟩