rainbow.math.sets.finset.filter

Finite sets src/rainbow/math/sets/finset/filter.clj2 definitions, 1 theorems

Certified predicates and extensional filtering for native Finsets.

decision/DecidablePred

decision/DecidablePred.{u} :
  (A : Sort u) (predicate : A → Prop)
  → Sort [:max [:max [:succ [:zero]] [:param u]] [:succ [:zero]]]

finset/filter

DefinitionSource, line 134

finset/filter.{u} :
  (A : Type u) (predicate : A → Prop) (decision : decision/DecidablePred A predicate)
  (source : finset/Finset A)
  → finset/Finset A

finset/filter-false

TheoremFor all inputsAxioms: sha256:312c762e43d05d2f04a321e6020f1a506f0da0fbca795b74fc29cebb2c23bcd7, sha256:9c1010a72238db722b25a1a515eae446d340534c5dff21bb5924e62561633c32, sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088Source, line 161

finset/filter-false.{u} :
  (A : Type u) (decision : decision/DecidablePred A (fun x₂ => proposition/falsity))
  (source : finset/Finset A)
  → finset/filter A (fun x₆ => proposition/falsity) decision source = finset/empty A

= = equality/Eq