Reference · Finite types, distributions and Markov chains

rainbow.math.finite.set-inverse-transport

Finite types, distributions and Markov chainssrc/rainbow/math/finite/set_inverse_transport.clj0 definitions, 5 theorems

Constructive finiteness and infinitude transport across explicit set inverses.

Depends onmath.sets.inverse-certificates

set/nonempty-of-maps-to.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A) (target : set/Set B)
  (maps-evidence : set/maps-to A B mapping source target)
  (source-nonempty-evidence : set/nonempty A source)
  → set/nonempty B target

set/nonempty-equivalent-of-mutual-maps.{u, v} :
  (A : Type u) (B : Type v) (forward : A → B) (backward : B → A) (source : set/Set A)
  (target : set/Set B) (forward-maps : set/maps-to A B forward source target)
  (backward-maps : set/maps-to B A backward target source)
  → proposition/conjunction (set/nonempty A source → set/nonempty B target) (set/nonempty B target → set/nonempty A source)

set/finite-equivalent-of-inverse.{u, v} :
  (A : Type u) (B : Type v) (forward : A → B) (backward : B → A) (source : set/Set A)
  (target : set/Set B) (forward-maps : set/maps-to A B forward source target)
  (backward-maps : set/maps-to B A backward target source)
  (inverse-evidence : set/inverse-on A B backward forward source target)
  → proposition/conjunction (set/finite A source → set/finite B target) (set/finite B target → set/finite A source)

set/infinite-equivalent-of-inverse.{u, v} :
  (A : Type u) (B : Type v) (forward : A → B) (backward : B → A) (source : set/Set A)
  (target : set/Set B) (forward-maps : set/maps-to A B forward source target)
  (backward-maps : set/maps-to B A backward target source)
  (inverse-evidence : set/inverse-on A B backward forward source target)
  → proposition/conjunction (set/infinite A source → set/infinite B target) (set/infinite B target → set/infinite A source)

set/finite-nonempty-equivalent-of-inverse.{u, v} :
  (A : Type u) (B : Type v) (forward : A → B) (backward : B → A) (source : set/Set A)
  (target : set/Set B) (forward-maps : set/maps-to A B forward source target)
  (backward-maps : set/maps-to B A backward target source)
  (inverse-evidence : set/inverse-on A B backward forward source target)
  → proposition/conjunction (conjunction → conjunction₁) (conjunction₁ → conjunction)
  where conjunction := proposition/conjunction (set/finite A source) (set/nonempty A source)
  where conjunction₁ := proposition/conjunction (set/finite B target) (set/nonempty B target)