Reference · Signed rationals

rainbow.math.rational.signed.distance-negate

Signed rationalssrc/rainbow/math/rational/signed/distance_negate.clj0 definitions, 1 theorems

d(-a,-b) ~ d(a,b): distance is invariant under negating both points. Needed for the negative branch of limit-product's distance-multiply (brick 2). Axiom-free; additive. Proof: distance p q = |p - q|; subtract(-a,-b) ~ negate(a-b) (from negate-additive on a and (negate b), since subtract reduces to add-with-negated-second); then |negate(a-b)| ~ |a-b| via absolute-negate.

Depends onmath.rational.signed.absolute-algebramath.rational.signed.distancemath.rational.signed.negate-additive

signed/distance-negate-both :
  (a b : ℚ)
  → signed/distance (signed/negate a) (signed/negate b) = signed/distance a b