Ineq datatype

This file contains an enum Ineq (whose constructors are eq, le, lt), and operations involving it. The type Ineq is one of the fundamental objects manipulated by the linarith and linear_combination tactics.

Inequalities

inductive Mathlib.Ineq : Type

The three-element type Ineq is used to represent the strength of a comparison between terms.

• eq : Ineq
• le : Ineq
• lt : Ineq

@[instance_reducible]

instance Mathlib.instDecidableEqIneq : DecidableEq Ineq

Equations

• Mathlib.instDecidableEqIneq x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Mathlib.instInhabitedIneq : Inhabited Ineq

Equations

• Mathlib.instInhabitedIneq = { default := Mathlib.instInhabitedIneq.default }

def Mathlib.instReprIneq.repr : Ineq → Nat → Std.Format

Equations

• Mathlib.instReprIneq.repr Mathlib.Ineq.eq prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mathlib.Ineq.eq")).group prec✝
• Mathlib.instReprIneq.repr Mathlib.Ineq.le prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mathlib.Ineq.le")).group prec✝
• Mathlib.instReprIneq.repr Mathlib.Ineq.lt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mathlib.Ineq.lt")).group prec✝

@[instance_reducible]

instance Mathlib.instReprIneq : Repr Ineq

Equations

• Mathlib.instReprIneq = { reprPrec := Mathlib.instReprIneq.repr }

def Mathlib.Ineq.max : Ineq → Ineq → Ineq

max R1 R2 computes the strength of the sum of two inequalities. If t1 R1 0 and t2 R2 0, then t1 + t2 (max R1 R2) 0.

Equations

• Mathlib.Ineq.lt.max x✝ = Mathlib.Ineq.lt
• x✝.max Mathlib.Ineq.lt = Mathlib.Ineq.lt
• Mathlib.Ineq.le.max x✝ = Mathlib.Ineq.le
• x✝.max Mathlib.Ineq.le = Mathlib.Ineq.le
• Mathlib.Ineq.eq.max Mathlib.Ineq.eq = Mathlib.Ineq.eq

def Mathlib.Ineq.cmp : Ineq → Ineq → Ordering

Ineq is ordered eq < le < lt.

Equations

• Mathlib.Ineq.eq.cmp Mathlib.Ineq.eq = Ordering.eq
• Mathlib.Ineq.eq.cmp x✝ = Ordering.lt
• Mathlib.Ineq.le.cmp Mathlib.Ineq.le = Ordering.eq
• Mathlib.Ineq.le.cmp Mathlib.Ineq.lt = Ordering.lt
• Mathlib.Ineq.lt.cmp Mathlib.Ineq.lt = Ordering.eq
• x✝¹.cmp x✝ = Ordering.gt

def Mathlib.Ineq.toString : Ineq → String

Prints an Ineq as the corresponding infix symbol.

Equations

• Mathlib.Ineq.eq.toString = "="
• Mathlib.Ineq.le.toString = "≤"
• Mathlib.Ineq.lt.toString = "<"

@[instance_reducible]

instance Mathlib.Ineq.instToString : ToString Ineq

Equations

• Mathlib.Ineq.instToString = { toString := Mathlib.Ineq.toString }