norm_ofNormedAddCommGroup_le — Mathlib

English

If f is continuous and bounded by C (i.e., ∀x, ‖f(x)‖ ≤ C), then the norm of the corresponding bounded continuous function is at most C.

Русский

Пусть f — непрерывная функция, предел которой по норме не превышает C; тогда нормa соответствующей ограниченной непрерывной функции не превосходит C.

LaTeX

$$$\|\operatorname{ofNormedAddCommGroup} f\, H_f\, C\, H\| \le C$$$

Lean4

theorem norm_ofNormedAddCommGroup_le {f : α → β} (hfc : Continuous f) {C : ℝ} (hC : 0 ≤ C) (hfC : ∀ x, ‖f x‖ ≤ C) :
    ‖ofNormedAddCommGroup f hfc C hfC‖ ≤ C :=
  (norm_le hC).2 hfC

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