Reference · Signed rationals

rainbow.math.rational.signed.strict-order

Signed rationalssrc/rainbow/math/rational/signed/strict_order.clj0 definitions, 8 theorems

Strict order on signed rationals -- the foundation strict convexity (and unique-minimizer results) need, which the non-strict `signed/at-most` lane lacked. signed/less-than x y := (at-most x y) AND (not (equivalent x y)) [reducible] signed/less-than-intro : at-most x y -> not(x~y) -> x<y signed/less-than-implies-at-most : x<y -> at-most x y signed/less-than-irreflexive : not (x<x) signed/less-than-asymmetric : x<y -> not (y<x) Built on the intuitionistic-logic layer (proposition/conjunction, /negation = P->falsity, /conjoin, /left, /right) plus at-most-antisymmetric and equivalent-reflexive. Irreflexivity feeds x~x (reflexivity) to the negation component; asymmetry derives x~y from at-most both ways (antisymmetry) and contradicts the negation component. Transitivity and strict monotonicity are the next bricks. Wall-free; does not touch the LP checker.

Depends onmath.rational.signed.limit-uniquenessmath.rational.signed.order-transitivitymath.rational.signed.order-respects

signed/less-than :
  (x₁ x₂ : ℚ)
  → Prop

signed/less-than-intro :
  (x y : ℚ)
  (le : x ≤ y)
  (neq : proposition/negation (x = y))
  → x < y

signed/less-than-implies-at-most :
  (x y : ℚ)
  (h : x < y)
  → x ≤ y

signed/less-than-irreflexive :
  (x : ℚ)
  → proposition/negation (x < x)

signed/less-than-asymmetric :
  (x y : ℚ)
  (hxy : x < y)
  → proposition/negation (y < x)

signed/less-than-transitive :
  (x y z : ℚ)
  (hxy : x < y)
  (hyz : y < z)
  → x < z

signed/less-than-of-at-most-of-less-than :
  (x y z : ℚ)
  (hle : x ≤ y)
  (hyz : y < z)
  → x < z

signed/less-than-of-less-than-of-at-most :
  (x y z : ℚ)
  (hxy : x < y)
  (hle : y ≤ z)
  → x < z