bound — Mathlib

English

There exists a nonnegative bound C such that for all x, the norm of f(x) is at most C times the norm of x.

Русский

Существует неотрицательная константа C такая, что для любого x выполняется \\|f(x)\\| ≤ C \\|x\\|.

LaTeX

$$$\\exists C>0,\\ \\forall x,\\ ‖f x‖ ≤ C\\,‖x‖$$$

Lean4

theorem bound : ∃ C, 0 < C ∧ ∀ x, ‖f x‖ ≤ C * ‖x‖ :=
  let ⟨_C, hC⟩ := f.bound'
  exists_pos_bound_of_bound _ hC

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