exists_lt_norm

Mathlib.Analysis.Normed.Field.Basic

URI: https://scilib.ai/kg/mathlib#NormedField.exists_lt_norm

← MathLib Explorer

English

For every real number r, there exists x ∈ α such that r < ∥x∥.

Русский

Для каждого вещественного числа r существует x ∈ α такое, что r < ∥x∥.

LaTeX

$$$ \forall r \in \mathbb{R}, \exists x : α, r < \|x\| $$$

Lean4

theorem exists_lt_norm (r : ℝ) : ∃ x : α, r < ‖x‖ :=
  let ⟨w, hw⟩ := exists_one_lt_norm α
  let ⟨n, hn⟩ := pow_unbounded_of_one_lt r hw
  ⟨w ^ n, by rwa [norm_pow]⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru