Reference · Finite types, distributions and Markov chains

rainbow.math.finite.set-lattice

Finite types, distributions and Markov chainssrc/rainbow/math/finite/set_lattice.clj0 definitions, 4 theorems

Finite-set closure facts for complements, intersections, and suprema.

set/finite-complement-universal.{u} :
  (A : Type u) (inhabited : set/nonempty A (set/universal A))
  → set/finite A (set/complement A (set/universal A))

set/finite-complement-intersection.{u} :
  (A : Type u) (left right : set/Set A)
  (left-open : ∀ (left-nonempty-evidence : set/nonempty A left), set/finite A (set/complement A left))
  (right-open : ∀ (right-nonempty-evidence : set/nonempty A right), set/finite A (set/complement A right))
  (overlap-nonempty-evidence : set/nonempty A (set/intersection A left right))
  → set/finite A (complement)
  where complement := set/complement A (set/intersection A left right)

set/finite-complement-supremum.{u} :
  (A : Type u) (family : set/Set (set/Set A))
  (member-open : ∀ (source : set/Set A), ∀ (source-member : family source), ∀ (source-nonempty-evidence : set/nonempty A source), set/finite A (set/complement A source))
  (joined-nonempty-evidence : set/nonempty A (set/supremum A family))
  → set/finite A (complement)
  where complement := set/complement A (set/supremum A family)

set/infinite-intersection-of-finite-difference.{u} :
  (A : Type u) (left right : set/Set A) (left-infinite : set/infinite A left)
  (difference-finite : set/finite A (set/difference A left right))
  → set/infinite A (set/intersection A left right)