Reference · Natural numbers

rainbow.math.nat.distance-core

Natural numberssrc/rainbow/math/nat/distance_core.clj0 definitions, 6 theorems

Constructive zero and identity laws for computational natural distance.

nat/distance-zero-left :
  (value : ℕ)
  → nat/distance 0 value = value

nat/distance-zero-right :
  (value : ℕ)
  → nat/distance value 0 = value

nat/distance-self :
  (value : ℕ)
  → nat/distance value value = 0

nat/equal-of-distance-zero :
  (left right : ℕ)
  (same : nat/distance left right = 0)
  → left = right

nat/distance-zero-of-equal :
  (left right : ℕ)
  (same : left = right)
  → nat/distance left right = 0

nat/distance-zero-equivalent-equal :
  (left right : ℕ)
  → proposition/conjunction (nat/distance left right = 0 → left = right) (left = right → nat/distance left right = 0)