Reference · Finite sums

rainbow.math.sums.binary-conflicts

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

Reusable bridges from binary entries and nonpositive nonnegative sums to exclusions.

Depends onmath.sums.boolean-predicatemath.sums.nonneg-zeromath.rational.signed.strict-order

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

signed/nonnegative-nonpositive-sum-term-zero :
  (F : ℕ → ℚ) (n : ℕ)
  (nonnegative : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ F idx)
  (nonpositive : signed/expr-sum-value F n ≤ 0)
  (i : ℕ) (bound : nat/strict-below i n)
  → F i = 0

signed/binary-exclusion-zero-product :
  (x y z : ℚ) (xb : proposition/disjunction (x = 0) (x = 1))
  (yb : proposition/disjunction (y = 0) (y = 1))
  (excluded : x = 1 → y = 1 → z = 0)
  → x · (y · z) = 0