mem_nonneg

Mathlib.Algebra.Ring.Subsemiring.Order

URI: https://scilib.ai/kg/mathlib#Subsemiring.mem_nonneg

English

For every x in R, x belongs to nonneg R iff 0 ≤ x.

Русский

Для каждого x в R верно: x принадлежит nonneg R тогда и только тогда, когда 0 ≤ x.

LaTeX

$$$x \\in \\text{nonneg}(R) \\;\\iff\\; 0 \\le x$$$

Lean4

@[simp]
theorem mem_nonneg {x : R} : x ∈ nonneg R ↔ 0 ≤ x :=
  .rfl

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

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

Разделы

Аффилиация

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