Macros§
- assert_
isets_ equal - Prove two sets equal by extensionality. Usage is:
Functions§
- axiom_
iset_ is_ empty - group_
iset_ lib_ default - group_
iset_ properties - lemma_
int_ range - lemma_
iset_ difference2 - lemma_
iset_ difference_ len - lemma_
iset_ disjoint - lemma_
iset_ disjoint_ iff_ empty_ intersection - lemma_
iset_ disjoint_ lens - lemma_
iset_ empty_ equivalency_ len - lemma_
iset_ insert_ finite_ iff - lemma_
iset_ intersect_ again1 - lemma_
iset_ intersect_ again2 - lemma_
iset_ intersect_ union_ lens - lemma_
iset_ is_ empty_ len0 - lemma_
iset_ remove_ finite_ iff - lemma_
iset_ subset_ finite - lemma_
iset_ union_ again1 - lemma_
iset_ union_ again2 - lemma_
iset_ union_ finite_ iff - lemma_
iset_ union_ finite_ implies_ sets_ finite - lemma_
isets_ eq_ iff_ injective_ map_ eq - lemma_
isets_ eq_ iff_ injective_ map_ on_ eq - lemma_
len_ difference - lemma_
len_ intersect - lemma_
len_ subset - lemma_
len_ union - lemma_
len_ union_ ind - lemma_
map_ size - lemma_
map_ size_ bound - lemma_
subset_ equality - set_
int_ range