bounds_bddBelow — Mathlib

English

The set of admissible bounds is bounded below by 0; in particular, every admissible bound is nonnegative.

Русский

Множество допустимых границ ограничено снизу нулём; в частности, каждая допустимая граница неотрицательна.

LaTeX

$$$\\forall c \\in \\{t \\in \\mathbb{R} \\mid 0 \\le t \\wedge \\forall x, \\|f x\\| \\le t \\|x\\|\\},\\ 0 \\le c$$$

Lean4

theorem bounds_bddBelow {f : E →SL[σ₁₂] F} : BddBelow {c | 0 ≤ c ∧ ∀ x, ‖f x‖ ≤ c * ‖x‖} :=
  ⟨0, fun _ ⟨hn, _⟩ => hn⟩

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