uniformContinuous_of_continuous — Mathlib

English

A function with compact multiplier support which is continuous is uniformly continuous.

Русский

Функция с компактной поддержкой умножения и непрерывна, значит, равномерно непрерывна.

LaTeX

$$\\text{HasCompactMulSupport}(f) \\land \\text{Continuous}(f) \\Rightarrow \\text{UniformContinuous}(f)$$

Lean4

@[to_additive]
theorem uniformContinuous_of_continuous {f : α → β} [One β] (h1 : HasCompactMulSupport f) (h2 : Continuous f) :
    UniformContinuous f :=
  h2.uniformContinuous_of_tendsto_cocompact h1.is_one_at_infty

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