enorm_ne_zero'

Mathlib.Analysis.Normed.Group.Basic

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

English

The EN-norm of a is nonzero exactly when a is not the identity: ‖a‖ₑ ≠ 0 ↔ a ≠ 1.

Русский

Норма EN не нуль тогда, когда a не тождественно единице: ‖a‖ₑ ≠ 0 ↔ a ≠ 1.

LaTeX

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

Lean4

@[to_additive enorm_ne_zero]
theorem enorm_ne_zero' {a : E} : ‖a‖ₑ ≠ 0 ↔ a ≠ 1 :=
  enorm_eq_zero'.ne

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

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

Разделы

Аффилиация

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