Reference · Logic

rainbow.math.logic.infinite-transport

Logic src/rainbow/math/logic/infinite_transport.clj1 definitions, 5 theorems

Sort-polymorphic infinitude transport and a faithful native Int model.

int/to-nat

int/to-nat :
  (x₁ : data/Int)
  → ℕ

ℕ = data/Nat

list/sort-membership-map

TheoremFor all inputsNo axiomsSource, line 96

list/sort-membership-map.{l, m} :
  (A : Sort l) (B : Sort m) (mapping : A → B) (enumeration : List A) (value : A)
  (member : list/sort-membership A enumeration value)
  → list/sort-membership B (list/map A B mapping enumeration) (mapping value)

List = data/List

type/finite-of-surjection

TheoremFor all inputsNo axiomsSource, line 175

type/finite-of-surjection.{l, m} :
  (A : Sort l) (B : Sort m) (mapping : A → B)
  (onto : ∀ (target : B), proposition/existence A (fun source => mapping source = target))
  (source-finite : type/finite A)
  → type/finite B

= = equality/Eq

type/infinite-of-surjection

TheoremFor all inputsNo axiomsSource, line 228

type/infinite-of-surjection.{l, m} :
  (A : Sort l) (B : Sort m) (target-infinite : type/infinite B) (mapping : A → B)
  (onto : ∀ (target : B), proposition/existence A (fun source => mapping source = target))
  → type/infinite A

= = equality/Eq

int/to-nat-surjective

TheoremFor all inputsNo axiomsSource, line 254

int/to-nat-surjective :
  (target : ℕ)
  → proposition/existence data/Int (fun source => int/to-nat source = target)

= = equality/Eqℕ = data/Nat

type/infinite-int

TheoremWorked exampleNo axiomsSource, line 271

type/infinite-int :
  → type/infinite data/Int