exists_pos_norm_le' — Mathlib

English

If s is a bounded set in a seminormed group, there exists a positive real R such that for all x in s, ‖x‖ ≤ R.

Русский

Если множество s ограничено в семиномированной группе, существует положительная константа R such that для всех x ∈ s выполняется ‖x‖ ≤ R.

LaTeX

$$$\ exists R>0,\; \forall x\in s,\; \|x\| \le R.$$$

Lean4

@[to_additive exists_pos_norm_le]
theorem exists_pos_norm_le' (hs : IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R :=
  let ⟨R₀, hR₀⟩ := hs.exists_norm_le'
  ⟨max R₀ 1, by positivity, fun x hx => (hR₀ x hx).trans <| le_max_left _ _⟩

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