exists_forall_norm_le — Mathlib

English

For any simple function f: α → F into a normed group, there exists a bound C such that ∥f(x)∥ ≤ C for all x.

Русский

Для любой простой функции f: α → F существует константа C, такая что ∥f(x)∥ ≤ C для всех x.

LaTeX

$$$\\exists C, \\forall x, \\|f(x)\\| ≤ C.$$$

Lean4

theorem exists_forall_norm_le (f : α →ₛ F) : ∃ C, ∀ x, ‖f x‖ ≤ C :=
  exists_forall_le (f.map fun x => ‖x‖)

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