summaryrefslogtreecommitdiff
path: root/library/set
AgeCommit message (Collapse)Author
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