bounds_bddBelow — Mathlib

English

The set of nonnegative bounds bounding all values f(x) is bounded below by 0.

Русский

Множество неотрицательных ограничений, ограничивающих все значения f(x), ограничено снизу нулём.

LaTeX

$$$\\operatorname{BoundedBelow}\\{c:\\mathbb{R} : 0\\le c ∧ ∀x, ‖f x‖ ≤ c ‖x‖\\}$$$

Lean4

theorem bounds_bddBelow {f : NormedAddGroupHom V₁ V₂} : BddBelow {c | 0 ≤ c ∧ ∀ x, ‖f x‖ ≤ c * ‖x‖} :=
  ⟨0, fun _ ⟨hn, _⟩ => hn⟩

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