English
Let E and F be normed spaces over a nontrivial field 𝕜, and let {v_i} be a finite basis of E. If a bounded linear map u: E → F satisfies ||u(v_i)|| ≤ M for all i, then the operator norm of u is controlled by M, i.e., there exists a constant C > 0 such that ||u|| ≤ C·M for all such u and M.
Русский
Пусть E и F — нормированные пространства над непустым полем 𝕜, пусть {v_i} — конечный базис E. Если линейное ограниченное отображение u: E → F удовлетворяет ||u(v_i)|| ≤ M для всех i, то существует константа C > 0 такая, что ||u|| ≤ C·M для всех таких u и M.
LaTeX
$$$\\\\exists C > 0,\\\\forall u : E \\\\to_L[\\\\mathbb{K}] F,\\\\forall M \\\\in \\\\mathbb{R}, 0 \\le M \\\\Rightarrow (\\\\forall i \\\\in ι, \\\\\\|u(v_i)\\\\| \\le M) \\\\\\Rightarrow \\\\|u\\\\| \\\\le C \\\\cdot M$$$
Lean4
/-- A weaker version of `Basis.opNorm_le` that abstracts away the value of `C`. -/
theorem exists_opNorm_le {ι : Type*} [Finite ι] (v : Basis ι 𝕜 E) :
∃ C > (0 : ℝ), ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ i, ‖u (v i)‖ ≤ M) → ‖u‖ ≤ C * M :=
by
obtain ⟨C, hC, h⟩ := v.exists_opNNNorm_le (F := F)
refine ⟨C, hC, ?_⟩
intro u M hM H
simpa using h ⟨M, hM⟩ H
