Reference · Finite types, distributions and Markov chains

rainbow.math.finite.type

Finite types, distributions and Markov chains src/rainbow/math/finite/type.clj3 definitions, 5 theorems

Native finite and infinite carrier propositions as finite List covers.

list/sort-membership

list/sort-membership.{l} :
  (A : Sort l) (source : List A) (value : A)
  → Prop

List = data/List

type/finite

DefinitionSource, line 61

type/finite.{l} :
  (A : Sort l)
  → Prop

type/infinite

DefinitionSource, line 71

type/infinite.{l} :
  (A : Sort l)
  → Prop

type/finite-universal-equivalence

TheoremFor all inputsNo axiomsSource, line 272

type/finite-universal-equivalence.{u} :
  (A : Type u)
  → proposition/conjunction (set/finite A (set/universal A) → type/finite A) (type/finite A → set/finite A (set/universal A))

type/finite-of-finite-universal

TheoremFor all inputsNo axiomsSource, line 290

type/finite-of-finite-universal.{u} :
  (A : Type u) (evidence : set/finite A (set/universal A))
  → type/finite A

type/infinite-universal-equivalence

TheoremFor all inputsNo axiomsSource, line 310

type/infinite-universal-equivalence.{u} :
  (A : Type u)
  → proposition/conjunction (set/infinite A (set/universal A) → type/infinite A) (type/infinite A → set/infinite A (set/universal A))

type/finite-of-not-infinite

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366Source, line 335

type/finite-of-not-infinite.{u} :
  (A : Type u) (double-negation : type/infinite A → proposition/falsity)
  → type/finite A

type/infinite-product-equivalence

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366Source, line 400

type/infinite-product-equivalence.{u, v} :
  (A : Type u) (B : Type v)
  → proposition/conjunction (type/infinite (data/Product A B) → disjunction) (disjunction → type/infinite (data/Product A B))
  where disjunction := proposition/disjunction (proposition/conjunction (type/infinite A) (proposition/nonempty B)) (proposition/conjunction (proposition/nonempty A) (type/infinite B))