bounds_nonempty — Mathlib

English

There exists a nonnegative real bound M such that ∥f x∥ ≤ M ∥x∥ for all x.

Русский

Существуют некоторые неотрицательные числа M такие, что ∥f x∥ ≤ M ∥x∥ для всех x.

LaTeX

$$$\\exists M \\in \\mathbb{R},\\ M \\ge 0 \\text{ и } \\forall x, \\|f x\\| \\le M \\|x\\|$$$

Lean4

theorem bounds_nonempty [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} : ∃ c, c ∈ {c | 0 ≤ c ∧ ∀ x, ‖f x‖ ≤ c * ‖x‖} :=
  let ⟨M, hMp, hMb⟩ := f.bound
  ⟨M, le_of_lt hMp, hMb⟩

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