Ineq

Mathlib.Data.Ineq

URI: https://scilib.ai/kg/mathlib#Mathlib.Ineq

Lean4

/-- The three-element type `Ineq` is used to represent the strength of a comparison between
terms. -/
inductive Ineq : Type
  | eq
  | le
  | lt
  deriving DecidableEq, Inhabited, Repr

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

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

Разделы

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

Аффилиация

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