Reference · Non-negative rationals

rainbow.math.rational.nnrat.half-positive

Non-negative rationalssrc/rainbow/math/rational/nnrat/half_positive.clj0 definitions, 1 theorems

nnrat/half-positive : 0 < half (as the reducible conjunction 0<=half AND not(0~half)). half ~ 0 unfolds (defeq) to equality Nat (succ zero) zero (num(half)*den(0) reduces to succ zero, num(0)*den(half) to zero), so it is refuted exactly like nnrat/one-not-equivalent-zero -- no multiply lemmas needed, keeping the dependency chain minimal (farkas only, for zero-at-most). Provides the positive symmetric weight for strict-convexity minimizer uniqueness.

Depends onmath.rational.nnrat.farkas-elim-list

nnrat/half-positive :
  → proposition/conjunction (0 ≤ nnrat/half) (proposition/negation (0 = nnrat/half))