rainbow.math.sums.binary-mutuality

Finite sums src/rainbow/math/sums/binary_mutuality.clj0 definitions, 1 theorems

Mutual selected-edge implications identify binary entries.

signed/binary-mutual-selection-implies-equivalence

TheoremFor all inputsNo axiomsSource

signed/binary-mutual-selection-implies-equivalence :
  (x y : ℚ) (xb : proposition/disjunction (x = 0) (x = 1))
  (yb : proposition/disjunction (y = 0) (y = 1))
  (forward : x = 1 → y = 1)
  (reverse : y = 1 → x = 1)
  → x = y

0 = signed/zero1 = signed/one= = signed/equivalent: equality of rational valuesℚ = signed/SignedRational