uniformContinuous_of_bound — Mathlib

English

Let E and F be seminormed groups and f a homomorphism. If there exists a real constant C such that for all x, ∥f x∥ ≤ C ∥x∥, then f is uniformly continuous.

Русский

Пусть E и F — полугруппы с нормами, f — гомоморфизм. Если существует постоянная C ∈ ℝ такая, что для любого x выполняется ∥f x∥ ≤ C ∥x∥, то f равносильно является равномерно непрерывной.

LaTeX

$$$\left( \exists C \in \mathbb{R}, \ \forall x, \ \|f x\| \le C \|x\| \right) \Rightarrow \mathrm{UniformContinuous}(f).$$$

Lean4

@[to_additive]
theorem uniformContinuous_of_bound [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) :
    UniformContinuous f :=
  (MonoidHomClass.lipschitz_of_bound f C h).uniformContinuous

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