uniformContinuous_eval_of_mem — Mathlib

English

If x ∈ s and s ∈ 𝔖, then the evaluation map at x, composed with the 𝔖-restriction-toFun, is uniformly continuous on α →ᵤ[𝔖] β.

Русский

Пусть x ∈ s и s ∈ 𝔖. Тогда оценочная карта по координате x, композиция с ограничением по 𝔖, является равномерно непрерывной на пространстве функций α →ᵤ[𝔖] β.

LaTeX

$$$(h_{xs} : x \\in s) \\land (hs : s \\in 𝔖) \\Rightarrow \\mathrm{UniformContinuous}((\\mathrm{Function.eval}\\ x) \\circ \\mathrm{toFun}\\ 𝔖).$$$

Lean4

/-- If `x : α` is in some `S ∈ 𝔖`, then evaluation at `x` is uniformly continuous on
`α →ᵤ[𝔖] β`. -/
theorem uniformContinuous_eval_of_mem {x : α} (hxs : x ∈ s) (hs : s ∈ 𝔖) :
    UniformContinuous ((Function.eval x : (α → β) → β) ∘ toFun 𝔖) :=
  (UniformFun.uniformContinuous_eval β (⟨x, hxs⟩ : s)).comp (UniformOnFun.uniformContinuous_restrict α β 𝔖 hs)

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