rainbow.math.rational.nnrat.weighted-term-bound

Scalar weighted-term monotonicity for the finite mixture proof.

nnrat/weighted-term-at-most

TheoremFor all inputsNo axiomsSource, line 11

nnrat/weighted-term-at-most :
  (weight distance rho : ℚ≥0)
  (h : distance ≤ rho)
  → weight · distance ≤ weight · rho

· = nnrat/multiplyℚ≥0 = nnrat/NonnegativeRational≤ = nnrat/at-most