Reference · Finite sums

rainbow.math.sums.strict-indicator

Finite sumssrc/rainbow/math/sums/strict_indicator.clj0 definitions, 3 theorems

A strict comparison indicator is one exactly when the reverse weak inequality is false.

Depends onmath.sums.lp-boundsmath.rational.signed.decide-completenessmath.rational.signed.strict-order

signed/strict-comparison-indicator-nonnegative :
  (x y : ℚ)
  → 0 ≤ data/Bool.rec (fun x₄ => ℚ) 1 0 (signed/decide-at-most x y)

signed/strict-comparison-indicator-implies-not-at-most :
  (x y : ℚ)
  (indicator : 1 ≤ data/Bool.rec (fun x₄ => ℚ) 1 0 (signed/decide-at-most x y))
  → proposition/negation (x ≤ y)

signed/not-at-most-implies-strict-comparison-indicator :
  (x y : ℚ) (strict : proposition/negation (x ≤ y))
  → data/Bool.rec (fun x₄ => ℚ) 1 0 (signed/decide-at-most x y) = 1