Reference · Finite sums

rainbow.math.sums.admissions-block

Finite sumssrc/rainbow/math/sums/admissions_block.clj0 definitions, 2 theorems

A blocking indicator vanishes exactly when the student does not improve, or the college has neither vacancy nor rank improvement.

Depends onmath.sums.indicator-zeromath.rational.signed.no-zero-divisors

signed/admissions-block-implies-preferences :
  (a c d : ℚ)
  (nonpositive : data/Bool.rec (fun x₄ => ℚ) 1 0 (signed/decide-at-most 0 a) · (data/Bool.rec (fun x₈ => ℚ) 1 0 (signed/decide-at-most c 0) + data/Bool.rec (fun x₁₂ => ℚ) 1 0 (signed/decide-at-most 0 d)) ≤ 0)
  → proposition/disjunction (0 ≤ a) (proposition/conjunction (c ≤ 0) (0 ≤ d))

signed/admissions-preferences-imply-zero-block :
  (a c d : ℚ)
  (preferences : proposition/disjunction (0 ≤ a) (proposition/conjunction (c ≤ 0) (0 ≤ d)))
  → data/Bool.rec (fun x₄ => ℚ) 1 0 (signed/decide-at-most 0 a) · (data/Bool.rec (fun x₈ => ℚ) 1 0 (signed/decide-at-most c 0) + data/Bool.rec (fun x₁₂ => ℚ) 1 0 (signed/decide-at-most 0 d)) ≤ 0