Skip to content
Flexiana
Menu
Solutions
How we work
Research
Work
Products
Company
Bring us a hard problem
Rainbow docs menu

Reference · Non-negative rationals

rainbow.math.rational.nnrat.map-sum-member

Non-negative rationalssrc/rainbow/math/rational/nnrat/map_sum_member.clj0 definitions, 1 theorems

A listed nonnegative rational term is bounded by its finite sum. Constructive membership induction; no decidable equality, normalization, or duplicate-freedom premise. Kernel-checked and axiom-free on D63.

Depends onmath.rational.nnrat.metric-separation

nnrat/map-sum-at-least-member

TheoremFor all inputsNo axiomsSource, line 39

nnrat/map-sum-at-least-member.{u} :
  (A : Type u) (mapping : A → ℚ≥0) (items : List A) (selected : A)
  (member : list/membership A items selected)
  → mapping selected ≤ nnrat/map-sum A mapping items

List = data/Listℚ≥0 = nnrat/NonnegativeRational≤ = nnrat/at-most