uniformContinuous_eval — Mathlib

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⟩

Похожие утверждения