coe_nonneg

Mathlib.Algebra.Order.Ring.Cone

URI: https://scilib.ai/kg/mathlib#RingCone.coe_nonneg

English

The set of nonnegative elements is precisely the set {x ∈ T | 0 ≤ x} as a ring cone's carrier.

Русский

Набор неотрицательных элементов равен множеству {x ∈ T | 0 ≤ x} как носитель конуса кольца.

LaTeX

$$$ \\mathrm{nonneg}\\, T = \\{ x \\in T \\mid 0 \\le x \\}. $$$

Lean4

@[simp, norm_cast]
theorem coe_nonneg : nonneg T = {x : T | 0 ≤ x} :=
  rfl

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

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

Разделы

Аффилиация

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