exists_lt_enorm

Mathlib.Analysis.Normed.Field.Basic

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

English

There exists x with 1 < ‖x‖ₑ.

Русский

Существует x такое, что 1 < ‖x‖ₑ.

LaTeX

$$$ \exists x : α, 1 < \|x\|_e $$$

Lean4

theorem exists_lt_enorm {r : ℝ≥0∞} (hr : r ≠ ∞) : ∃ x : α, r < ‖x‖ₑ :=
  by
  lift r to ℝ≥0 using hr
  exact mod_cast exists_lt_nnnorm α r

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

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

Разделы

Аффилиация

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