Reference · Finite sums

rainbow.math.sums.binary-capacity

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

For binary entries, x+y<=1 means selecting x excludes y.

Depends onmath.sums.zero-violations

signed/boolean-cases-at-most-one :
  (x : ℚ) (binary : proposition/disjunction (x = 0) (x = 1))
  → x ≤ 1

signed/binary-capacity-implies-exclusion :
  (x y : ℚ) (yb : proposition/disjunction (y = 0) (y = 1))
  (capacity : x + y + signed/negate 1 ≤ 0)
  (selected : x = 1)
  → y = 0

signed/binary-exclusion-implies-capacity :
  (x y : ℚ) (xb : proposition/disjunction (x = 0) (x = 1))
  (yb : proposition/disjunction (y = 0) (y = 1))
  (exclusion : x = 1 → y = 0)
  → x + y + signed/negate 1 ≤ 0