enorm_pos'

Mathlib.Analysis.Normed.Group.Basic

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

English

The EN-norm is positive exactly when the element is not the identity: 0 < ‖a‖ₑ ↔ a ≠ 1.

Русский

Положительность EN-нормы совпадает с неравенством относительно единицы: 0 < ‖a‖ₑ ↔ a ≠ 1.

LaTeX

$$$0 < \\|a\\|_\\varepsilon \\iff a \\neq 1$$$

Lean4

@[to_additive (attr := simp) enorm_pos]
theorem enorm_pos' {a : E} : 0 < ‖a‖ₑ ↔ a ≠ 1 :=
  pos_iff_ne_zero.trans enorm_ne_zero'

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

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

Разделы

Аффилиация

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