uniformContinuous_eval_of_mem_sUnion

English

If x ∈ ⋃₀ 𝔖, then evaluation at x is uniformly continuous on α →ᵤ[𝔖] β.

Русский

Если x принадлежит объединению ⋃₀ 𝔖, то оценка по x на пространстве α →ᵤ[𝔖] β равномерно непрерывна.

LaTeX

$$$(hx : x \\in \\bigcup 𝔖) \\Rightarrow \\mathrm{UniformContinuous}((\\mathrm{Function.eval}\\ x) \\circ \\mathrm{toFun} 𝔖).$$$

Lean4

theorem uniformContinuous_eval_of_mem_sUnion {x : α} (hx : x ∈ ⋃₀ 𝔖) :
    UniformContinuous ((Function.eval x : (α → β) → β) ∘ toFun 𝔖) :=
  let ⟨_s, hs, hxs⟩ := hx
  uniformContinuous_eval_of_mem _ _ hxs hs

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