Reference · Finite types, distributions and Markov chains

rainbow.math.finite.set-boundary

Finite types, distributions and Markov chainssrc/rainbow/math/finite/set_boundary.clj0 definitions, 6 theorems

Classical boundary facts for native finite and infinite sets. These proofs turn repeated finite/infinite dichotomy arguments into reusable Clojure data. The module is separate from both the constructive finite-set algebra and the finite-map transport layer so their historical proof and axiom profiles remain stable.

set/finite-or-infinite.{u} :
  (A : Type u) (source : set/Set A)
  → proposition/disjunction (set/finite A source) (set/infinite A source)

set/infinite-or-finite.{u} :
  (A : Type u) (source : set/Set A)
  → proposition/disjunction (set/infinite A source) (set/finite A source)

set/not-infinite-equivalence.{u} :
  (A : Type u) (source : set/Set A)
  → proposition/conjunction ((set/infinite A source → proposition/falsity) → set/finite A source) (set/finite A source → set/infinite A source → proposition/falsity)

set/infinite-nonempty.{u} :
  (A : Type u) (source : set/Set A) (infinite-evidence : set/infinite A source)
  → set/nonempty A source

set/finite-of-subsingleton.{u} :
  (A : Type u) (source : set/Set A) (subsingleton-evidence : set/subsingleton A source)
  → set/finite A source

set/infinite-nontrivial.{u} :
  (A : Type u) (source : set/Set A) (infinite-evidence : set/infinite A source)
  → set/nontrivial A source