uniformContinuous_eval — Mathlib

English

If the union of 𝔖 is all of α (i.e. ⋃₀ 𝔖 = univ), then for every x ∈ α the evaluation map is uniformly continuous.

Русский

Если объединение 𝔖 охватывает всю α (⋃₀ 𝔖 = univ), то для каждого x ∈ α оценка по x равномерно непрерывна.

LaTeX

$$$(h : \\bigcup 𝔖 = \\mathrm{univ}) \\Rightarrow \\forall x, \\mathrm{UniformContinuous}((\\mathrm{Function.eval}\\ x) \\circ toFun 𝔖).$$$

Lean4

theorem uniformContinuous_eval (h : ⋃₀ 𝔖 = univ) (x : α) :
    UniformContinuous ((Function.eval x : (α → β) → β) ∘ toFun 𝔖) :=
  uniformContinuous_eval_of_mem_sUnion _ _ <| h.symm ▸ mem_univ _

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