exists_pos_norm_lt' — Mathlib

English

If s is bounded, there exists R > 0 such that ∥x∥ < R for all x in s.

Русский

Если s ограничено, существует R > 0, такое что ∥x∥ < R для всех x ∈ s.

LaTeX

$$∃ R > 0, ∀ x ∈ s, ∥x∥ < R$$

Lean4

@[to_additive Bornology.IsBounded.exists_pos_norm_lt]
theorem exists_pos_norm_lt' (hs : IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ < R :=
  let ⟨R, hR₀, hR⟩ := hs.exists_pos_norm_le'
  ⟨R + 1, by positivity, fun x hx ↦ (hR x hx).trans_lt (lt_add_one _)⟩

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