nontrivial

Mathlib.Analysis.Normed.Ring.Basic

URI: https://scilib.ai/kg/mathlib#NormOneClass.nontrivial

English

If a norm-one class exists on a seminormed additive commutative group with one, then the group is nontrivial (there exist two distinct elements).

Русский

Если существует нормо-единица, то группа не тривиальна; существуют различные элементы.

LaTeX

$$$\exists x,y\ (x\neq y).$$$

Lean4

theorem nontrivial : Nontrivial G :=
  nontrivial_of_ne 0 1 <| ne_of_apply_ne norm <| by simp

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

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

Разделы

Аффилиация

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