summaryrefslogtreecommitdiff
path: root/library/set
AgeCommit message (Collapse)Author
6 hoursRemove some ZF stuffadelon
45 hoursComplete named construction premise viewsadelon
3 daysStabilize one-core set proofsadelon
4 daysMigrate equinumerosity proofsadelon
4 daysMigrate Cantor and fixpoint proofsadelon
4 daysSimplify exact product proofsadelon
4 daysMigrate filter proofs to exact checkingadelon
4 daysMigrate product proofs to exact checkingadelon
4 daysAlign successor with canonical set insertionadelon
Exact definitions remain named globals, so suc spells the canonical construction directly to coalesce with the packaged successor.
4 daysMigrate elementary set proofs to exact checkingadelon
4 daysRewrite protected set and naturals closureadelon
7 daysBuild module-local syntax interfacesadelon
2026-04-12Make handling of local variables stricteradelon
2025-12-03Update regularity.texadelon
2025-07-16Add quantified calcs and relax tokenizationadelon
Use an `\iff`-calc to speed up `union_as_unions`. Also remove `in_implies_neq` which seems to interact badly with the choice axiom used by superposition-based proofs like Vampire in cut-down problems.
2025-07-08Linting and optimizationadelon
2024-09-18working commitSimon-Kor
2024-05-28Pow closed under binary intersectionadelon
2024-05-23Update formattingadelon
2024-05-22Update filter.texadelon
2024-05-22Add filter lemmasadelon
2024-05-22Add lemma `filter_setminus_in`adelon
2024-05-21Add simple lemmas on filtersadelon
2024-02-10Initial commitadelon
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 19:09:35 +0000