bounds_nonempty — Mathlib

English

There exists a bound C such that 0 ≤ C and ∀ x, ‖f x‖ ≤ C‖x‖.

Русский

Существует ограничение C с условием 0 ≤ C и ∀x, ‖f x‖ ≤ C‖x‖.

LaTeX

$$$\\exists C: \\mathbb{R}, C≥0 ∧ ∀x, ‖f x‖ ≤ C ‖x‖$$$

Lean4

theorem bounds_nonempty {f : NormedAddGroupHom V₁ V₂} : ∃ c, c ∈ {c | 0 ≤ c ∧ ∀ x, ‖f x‖ ≤ c * ‖x‖} :=
  let ⟨M, hMp, hMb⟩ := f.bound
  ⟨M, le_of_lt hMp, hMb⟩

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