Reference · Non-negative rationals

rainbow.math.rational.nnrat.strict-order

Non-negative rationalssrc/rainbow/math/rational/nnrat/strict_order.clj0 definitions, 8 theorems

Strict order on nonnegative rationals -- the nnrat mirror of signed_strict_order, needed for the no-zero-divisors pair theorem (which case-splits on the nnrat order of a signed value's positive/negative components). nnrat/less-than x y := (at-most x y) AND (not (equivalent x y)) [reducible] + intro, implies-at-most, irreflexive, asymmetric, transitive, and the two <=/< mixing lemmas. Direct port of the signed strict order onto the nnrat order primitives. Wall-free.

Depends onmath.rational.nnrat.metric-separationalgorithms.proofs.decision-guarantee-auditmath.finite.policy-iteration

nnrat/less-than :
  (x₁ x₂ : ℚ≥0)
  → Prop

nnrat/less-than-intro :
  (x y : ℚ≥0)
  (le : x ≤ y)
  (neq : proposition/negation (x = y))
  → nnrat/less-than x y

nnrat/less-than-implies-at-most :
  (x y : ℚ≥0) (h : nnrat/less-than x y)
  → x ≤ y

nnrat/less-than-irreflexive :
  (x : ℚ≥0)
  → proposition/negation (nnrat/less-than x x)

nnrat/less-than-asymmetric :
  (x y : ℚ≥0) (hxy : nnrat/less-than x y)
  → proposition/negation (nnrat/less-than y x)

nnrat/less-than-transitive :
  (x y z : ℚ≥0) (hxy : nnrat/less-than x y) (hyz : nnrat/less-than y z)
  → nnrat/less-than x z

nnrat/less-than-of-at-most-of-less-than :
  (x y z : ℚ≥0)
  (hle : x ≤ y)
  (hyz : nnrat/less-than y z)
  → nnrat/less-than x z

nnrat/less-than-of-less-than-of-at-most :
  (x y z : ℚ≥0) (hxy : nnrat/less-than x y)
  (hle : y ≤ z)
  → nnrat/less-than x z