Reference · Logic

rainbow.math.logic.infinite-injection

Logicsrc/rainbow/math/logic/infinite_injection.clj0 definitions, 3 theorems

Classical, sort-polymorphic infinitude transport along injections.

list/preimage-representatives.{l, m} :
  (Source : Sort l) (Target : Sort m) (mapping : Source → Target)
  (injective : ∀ (left : Source), ∀ (right : Source), ∀ (same-image : mapping left = mapping right), left = right)
  (target-enumeration : List Target)
  → proposition/existence (List Source) (fun source-enumeration => ∀ (value : Source), ∀ (image-member : membership (mapping value)), list/sort-membership Source source-enumeration value)
  where membership := list/sort-membership Target target-enumeration

type/finite-of-injection.{l, m} :
  (Source : Sort l) (Target : Sort m) (mapping : Source → Target)
  (injective : ∀ (left : Source), ∀ (right : Source), ∀ (same-image : mapping left = mapping right), left = right)
  (target-finite : type/finite Target)
  → type/finite Source

type/infinite-of-injection.{l, m} :
  (A : Sort l) (B : Sort m) (source-infinite : type/infinite B) (mapping : B → A)
  (injective : ∀ (left : B), ∀ (right : B), ∀ (same-image : mapping left = mapping right), left = right)
  → type/infinite A