English
Let E and F be seminormed groups and f a homomorphism between them. If there exists a real constant C such that for all x, ∥f x∥ ≤ C ∥x∥, then f is continuous.
Русский
Пусть E и F — полугруппы с нормами, f — гомоморфизм между ними. Если существует постоянная C ∈ ℝ такая, что для всякого x выполняется ∥f x∥ ≤ C ∥x∥, то f непрерывен.
LaTeX
$$$\left( \exists C \in \mathbb{R}, \ \forall x \in E, \ \|f x\| \le C \|x\| \right) \Rightarrow \text{Continuous}(f).$$$
Lean4
/-- A homomorphism `f` of seminormed groups is continuous, if there exists a constant `C` such that
for all `x`, one has `‖f x‖ ≤ C * ‖x‖`. -/
@[to_additive /-- A homomorphism `f` of seminormed groups is continuous, if there exists a constant
`C` such that for all `x`, one has `‖f x‖ ≤ C * ‖x‖`. -/
]
theorem continuous_of_bound [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) : Continuous f :=
(MonoidHomClass.lipschitz_of_bound f C h).continuous
