zero_lt_one_add_norm_sq'

Mathlib.Analysis.Normed.Group.Basic

URI: https://scilib.ai/kg/mathlib#zero_lt_one_add_norm_sq'

English

For any x, 0 < 1 + ‖x‖^2.

Русский

Для любого x выполняется 0 < 1 + ‖x‖^2.

LaTeX

$$$0 < 1 + \|x\|^2$$$

Lean4

@[to_additive zero_lt_one_add_norm_sq]
theorem zero_lt_one_add_norm_sq' (x : E) : 0 < 1 + ‖x‖ ^ 2 := by positivity

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

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

Разделы

Аффилиация

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