of_gt

Mathlib.Algebra.Order.Monoid.Canonical.Defs

URI: https://scilib.ai/kg/mathlib#NeZero.of_gt

English

If x < y in an AddZeroClass with a canonically ordered add, then y is nonzero.

Русский

Если x < y в аддитивном канонически упорядоченном классе, то y ≠ 0.

LaTeX

$$x < y \Rightarrow y \neq 0$$

Lean4

theorem of_gt {M} [AddZeroClass M] [Preorder M] [CanonicallyOrderedAdd M] {x y : M} (h : x < y) : NeZero y :=
  of_pos <| pos_of_gt h

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

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

Разделы

Аффилиация

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