Reference · Natural numbers

rainbow.math.nat.metric-separation

Natural numberssrc/rainbow/math/nat/metric_separation.clj0 definitions, 5 theorems

Constructive positivity and separation laws for computational Nat distance.

nat/positive-of-nonzero :
  (value : ℕ) (nonzero : value = 0 → proposition/falsity)
  → nat/strict-below 0 value

nat/nonzero-of-positive :
  (value : ℕ) (positive : nat/strict-below 0 value)
  (h₁ : value = 0)
  → proposition/falsity

nat/distance-nonzero-of-not-equal :
  (left right : ℕ) (different : left = right → proposition/falsity)
  (h₁ : nat/distance left right = 0)
  → proposition/falsity

nat/distance-positive-of-not-equal :
  (left right : ℕ) (different : left = right → proposition/falsity)
  → nat/strict-below 0 (nat/distance left right)

nat/distance-positive-equivalent-not-equal :
  (left right : ℕ)
  → proposition/conjunction (below → left = right → proposition/falsity) ((left = right → proposition/falsity) → below)
  where below := nat/strict-below 0 (nat/distance left right)