Reference
Finite sets
5 modules in src/rainbow/math/sets/finset/. All folders
| Module | What it proves | Theorems |
|---|---|---|
| math.sets.finset.data | Computational finite sets: duplicate-free enumerations paired with proof data. | 6 |
| math.sets.finset.filter | Certified predicates and extensional filtering for native Finsets. | 1 |
| math.sets.finset.nontrivial | Nontrivial native Finsets through their extensional predicate view. | 4 |
| math.sets.finset.powerset | Finite-set powersets derived from extensional Set and Finset proof data. | 5 |
| math.sets.finset.range | Native initial segments of Nat and finite-Finset range bounds. | 11 |