exists_norm_lt

Mathlib.Analysis.Normed.Field.Basic

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

← MathLib Explorer

English

For any real r, there exists x with r < ∥x∥.

Русский

Для любого r существует x с r < ∥x∥.

LaTeX

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

Lean4

theorem exists_norm_lt {r : ℝ} (hr : 0 < r) : ∃ x : α, 0 < ‖x‖ ∧ ‖x‖ < r :=
  let ⟨w, hw⟩ := exists_lt_norm α r⁻¹
  ⟨w⁻¹, by rwa [← Set.mem_Ioo, norm_inv, ← Set.mem_inv, Set.inv_Ioo_0_left hr]⟩

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

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

Разделы

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

Аффилиация

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