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

Reference · Finite sets

rainbow.math.sets.finset.powerset

Finite setssrc/rainbow/math/sets/finset/powerset.clj1 definitions, 5 theorems

Finite-set powersets derived from extensional Set and Finset proof data.

finset/powerset

DefinitionSource, line 115

finset/powerset.{u} :
  (A : Type u) (source : finset/Finset A)
  → finset/Finset (finset/Finset A)

finset/member-powerset-equivalent-subset

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366, sha256:312c762e43d05d2f04a321e6020f1a506f0da0fbca795b74fc29cebb2c23bcd7, sha256:9c1010a72238db722b25a1a515eae446d340534c5dff21bb5924e62561633c32, sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 136

finset/member-powerset-equivalent-subset.{u} :
  (A : Type u) (source candidate : finset/Finset A)
  → proposition/conjunction (set → finset/subset A candidate source) (finset/subset A candidate source → set)
  where set := finset/to-set (finset/Finset A) (finset/powerset A source) candidate

finset/self-member-powerset

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366, sha256:312c762e43d05d2f04a321e6020f1a506f0da0fbca795b74fc29cebb2c23bcd7, sha256:9c1010a72238db722b25a1a515eae446d340534c5dff21bb5924e62561633c32, sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 155

finset/self-member-powerset.{u} :
  (A : Type u) (source : finset/Finset A)
  → finset/to-set (finset/Finset A) (finset/powerset A source) source

finset/powerset-monotone

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366, sha256:312c762e43d05d2f04a321e6020f1a506f0da0fbca795b74fc29cebb2c23bcd7, sha256:9c1010a72238db722b25a1a515eae446d340534c5dff21bb5924e62561633c32, sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 172

finset/powerset-monotone.{u} :
  (A : Type u) (left right : finset/Finset A)
  (left-subset-right : finset/subset A left right)
  → finset/subset (finset/Finset A) (finset/powerset A left) (finset/powerset A right)

finset/powerset-nonempty

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366, sha256:312c762e43d05d2f04a321e6020f1a506f0da0fbca795b74fc29cebb2c23bcd7, sha256:9c1010a72238db722b25a1a515eae446d340534c5dff21bb5924e62561633c32, sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 198

finset/powerset-nonempty.{u} :
  (A : Type u) (source : finset/Finset A)
  → finset/nonempty (finset/Finset A) (finset/powerset A source)

finset/powerset-injective

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366, sha256:312c762e43d05d2f04a321e6020f1a506f0da0fbca795b74fc29cebb2c23bcd7, sha256:9c1010a72238db722b25a1a515eae446d340534c5dff21bb5924e62561633c32, sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 222

finset/powerset-injective.{u} :
  (A : Type u) (left right : finset/Finset A)
  (same-image : (fun source => finset/powerset A source) left = (fun source => finset/powerset A source) right)
  → left = right

= = equality/Eq