of_ge

Mathlib.Algebra.Order.Monoid.Canonical.Defs

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

← MathLib Explorer

English

If x ≤ y and x ≠ 0, then y ≠ 0.

Русский

Если x ≤ y и x ≠ 0, тогда y ≠ 0.

LaTeX

$$x \le y \Rightarrow \mathrm{NeZero}(x) \Rightarrow \mathrm{NeZero}(y)$$

Lean4

theorem of_ge {M} [AddZeroClass M] [PartialOrder M] [CanonicallyOrderedAdd M] {x y : M} [NeZero x] (h : x ≤ y) :
    NeZero y :=
  of_pos <| lt_of_lt_of_le (pos x) h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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