Skip to content
Flexiana
Menu
Solutions
How we work
Research
Work
Products
Company
Bring us a hard problem
Rainbow docs menu

Reference · Finite types, distributions and Markov chains

rainbow.math.finite.powerset

Finite types, distributions and Markov chainssrc/rainbow/math/finite/powerset.clj1 definitions, 4 theorems

Finite powersets, infinite suprema, and subtype projection injectivity.

list/set-powerset

DefinitionSource, line 120

list/set-powerset.{u} :
  (A : Type u) (enumeration : List A)
  → List (set/Set A)

List = data/List

list/membership-set-powerset

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366, sha256:9c1010a72238db722b25a1a515eae446d340534c5dff21bb5924e62561633c32, sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 186

list/membership-set-powerset.{u} :
  (A : Type u) (enumeration : List A) (candidate : set/Set A)
  (covered : ∀ (value : A), ∀ (candidate-member : candidate value), list/membership A enumeration value)
  → list/membership (set/Set A) (list/set-powerset A enumeration) candidate

List = data/List

set/finite-powerset

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366, sha256:9c1010a72238db722b25a1a515eae446d340534c5dff21bb5924e62561633c32, sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 385

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

set/infinite-supremum

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366, sha256:9c1010a72238db722b25a1a515eae446d340534c5dff21bb5924e62561633c32, sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 446

set/infinite-supremum.{u} :
  (A : Type u) (family : set/Set (set/Set A))
  (family-infinite : set/infinite (set/Set A) family)
  → set/infinite A (set/supremum A family)

subtype/value-injective

TheoremFor all inputsAxioms: sha256:312c762e43d05d2f04a321e6020f1a506f0da0fbca795b74fc29cebb2c23bcd7Source, line 475

subtype/value-injective.{u} :
  (A : Type u) (source : set/Set A) (left right : data/Subtype A source)
  (same-image : subtype/value A source left = subtype/value A source right)
  → left = right

= = equality/Eq