Reference · Natural numbers

rainbow.math.nat.infinite

Natural numberssrc/rainbow/math/nat/infinite.clj3 definitions, 7 theorems

Axiom-free Nat constructor discrimination, list bounds, and infinitude.

nat/predecessor :
  (x₁ : ℕ)
  → ℕ

nat/strict-below :
  (x₁ x₂ : ℕ)
  → Prop

list/nat-bound :
  (x₁ : List ℕ)
  → ℕ

nat/zero-not-successor :
  (value : ℕ)
  (h₁ : 0 = data/succ value)
  → proposition/falsity

nat/successor-injective :
  (left right : ℕ)
  (same : data/succ left = data/succ right)
  → left = right

nat/add-associative :
  (left middle right : ℕ)
  → algebra/nat-add (algebra/nat-add left middle) right = algebra/nat-add left (algebra/nat-add middle right)

nat/add-commutative :
  (left right : ℕ)
  → algebra/nat-add left right = algebra/nat-add right left

nat/not-equal-successor-add :
  (value extra : ℕ)
  (h₁ : value = data/succ (algebra/nat-add value extra))
  → proposition/falsity

list/member-strictly-below-nat-bound :
  (enumeration : List ℕ) (value : ℕ) (member : list/membership ℕ enumeration value)
  → nat/strict-below value (list/nat-bound enumeration)

type/infinite-nat :
  → type/infinite ℕ