exists_pos_bound_of_bound — Mathlib

English

If a linear map f has a bound M on ∥f x∥ ≤ M∥x∥, there exists a positive bound N with ∥f x∥ ≤ N∥x∥ for all x.

Русский

Если линейный отображение имеет границу M, существует положительная граница N, такая что ∥f x∥ ≤ N∥x∥ для всех x.

LaTeX

$$$\\exists N>0,\\forall x, ∥f x∥ ≤ N ∥x∥$$$

Lean4

theorem exists_pos_bound_of_bound {V W : Type*} [SeminormedAddCommGroup V] [SeminormedAddCommGroup W] {f : V → W}
    (M : ℝ) (h : ∀ x, ‖f x‖ ≤ M * ‖x‖) : ∃ N, 0 < N ∧ ∀ x, ‖f x‖ ≤ N * ‖x‖ :=
  ⟨max M 1, lt_of_lt_of_le zero_lt_one (le_max_right _ _), fun x =>
    calc
      ‖f x‖ ≤ M * ‖x‖ := h x
      _ ≤ max M 1 * ‖x‖ := by gcongr; apply le_max_left⟩

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