Reference
Sets
16 modules in src/rainbow/math/sets/. All folders
| Module | What it proves | Theorems |
|---|---|---|
| math.sets.fiber-characterization | Image, surjection, and injection characterized by their source fibers. | 5 |
| math.sets.fiber-unique | Unique existence from subsingleton predicates, applied to bijection fibers. | 5 |
| math.sets.image-certificates | Constructive image/target inclusions from certified set maps. | 5 |
| math.sets.image-composition | The image of a composite map is the nested image, by mutual inclusion. | 6 |
| math.sets.image-difference | Images preserve set difference exactly when witnesses cannot collide. | 3 |
| math.sets.image-insert | Images commute constructively with inserting one source value. | 3 |
| math.sets.image-lattice | Images preserve unions, and preserve intersections under injectivity. | 6 |
| math.sets.image-preimage-adjunction | The constructive image/preimage Galois connection for set inclusion. | 3 |
| math.sets.inverse-certificates | Constructive injectivity, surjectivity, and bijectivity from set inverses. | 5 |
| math.sets.inverse-unique-fiber | Two-sided set inverses provide unique witnesses in every target fiber. | 4 |
| math.sets.map-composition | Constructive set-map properties preserved by function composition. | 8 |
| math.sets.preimage-composition | Identity and composition laws for set preimages. | 6 |
| math.sets.preimage-lattice | Preimages preserve intersection, union, and difference by exact reuse. | 9 |
| math.sets.range | Lean-compatible Set range ordering and native finite-range laws. | 1 |
| math.sets.range-image-bridge | Bridge global function ranges to images of universal source sets. | 4 |
| math.sets.range-surjective | Characterize surjections by their universal ranges. | 4 |