cmp

Mathlib.Tactic.Linarith.Oracle.FourierMotzkin

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Linarith.PComp.cmp

Lean4

/-- The `src : CompSource` field is ignored when comparing `PComp`s. Two `PComp`s proving the same
comparison, with different sources, are considered equivalent.
-/
def cmp (p1 p2 : PComp) : Ordering :=
  p1.c.cmp p2.c

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

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

Разделы

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

Аффилиация

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