Reference · Signed rationals

rainbow.math.rational.signed.reciprocal-nonnegative

Signed rationalssrc/rainbow/math/rational/signed/reciprocal_nonnegative.clj0 definitions, 1 theorems

B3 of the limit-reciprocal arc: the reciprocal of a nonnegative signed rational is nonnegative. signed/reciprocal-nonnegative : nonnegative x -> nonnegative (reciprocal x) Immediate from the sign-free definition reciprocal x = x * (1/(x*x)): the second factor 1/(x*x) = from-nnrat (recip mmag) is nonnegative (from-nnrat of any nnrat is >= 0, since its negative component is 0 -- nnrat/zero-at-most), so multiply-nonnegative closes it. Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.reciprocalmath.rational.signed.multiply-ordermath.rational.nnrat.farkas-elim-list

signed/reciprocal-nonnegative :
  (x : ℚ) (hx : signed/nonnegative x)
  → signed/nonnegative (signed/reciprocal x)