Menu

Rainbow docs menu

Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.bb-leaf-bound

Lemmas behind operations-research checks src/rainbow/math/lemmas/bb_leaf_bound.clj0 definitions, 1 theorems

General lemmas: bb leaf bound. The mathematical facts the corresponding checks rest on, each checked by the kernel.

Depends onmath.lemmas.lp-duality math.nat.infinite math.nat.strict-below-split math.nat.strict-below-more math.nat.at-most-add math.rational.nnrat.harmonic-convergence math.rational.signed.decide-order math.rational.signed.decide-reflexive math.nat.at-most-cancellation math.rational.nnrat.order-equivalence math.rational.nnrat.archimedean math.rational.nnrat.add-monotone math.rational.nnrat.add-cancellation math.rational.nnrat.additive-reassociation math.rational.signed.order-transitivity math.rational.signed.convergence math.rational.signed.order-respects math.rational.nnrat.identities math.rational.signed.limit-uniqueness math.logic.boolean-and math.rational.signed.decide-equivalence math.rational.signed.decide-completeness math.nat.divmod math.nat.pair-index-inverse math.rational.signed.strict-order math.rational.signed.multiply math.rational.nnrat.multiply-commute math.rational.nnrat.product-reassociation math.rational.nnrat.distribute-right math.rational.nnrat.ring math.rational.nnrat.multiply-monotone math.rational.nnrat.order-difference math.rational.signed.multiply-order math.rational.signed.equivalence-laws math.rational.nnrat.minmax math.rational.nnrat.farkas-elim-list math.rational.signed.no-zero-divisors math.rational.signed.unit-laws math.checks math.rational.signed.minmax math.rational.signed.minmax-algebra math.rational.signed.clamp math.rational.signed.deviation-rows math.rational.signed.absolute math.rational.signed.absolute-algebra math.rational.signed.distance math.nat.linear-order

nat/pair-index-below-rectangular

TheoremFor all inputsNo axiomsSource

nat/pair-index-below-rectangular :
  (n a b L : ℕ) (ha : nat/strict-below a n) (hb : nat/strict-below b L)
  → nat/strict-below (algebra/nat-add a (nat/multiply b n)) (nat/multiply L n)

ℕ = data/Nat