Reference · Non-negative rationals

rainbow.math.rational.nnrat.distance-translation

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

Removing common nonnegative mass preserves exact rational distance. The proof uses the additive-radius characterization in both directions, additive monotonicity, and cancellation; no truncated subtraction is assumed.

Depends onmath.rational.nnrat.metric-separationmath.rational.nnrat.add-cancellationmath.rational.nnrat.add-monotonemath.rational.nnrat.additive-reassociation

nnrat/distance-add-right :
  (a b common : ℚ≥0)
  → nnrat/distance (a + common) (b + common) = nnrat/distance a b