partition_disjoint_bigfcup lemma

math-comp / finmap

Finite sets, finite maps, multisets and generic sets

46 stars 28 forks source link

Closed affeldt-aist closed 3 years ago

affeldt-aist commented 4 years ago

on the model of the eponymous lemma in finset
~TODO: add the following to the changelog if PR #74 can be merged:~ DONE
```
Added:
```
in finmap.v:
- definitions cover and trivIset
- lemmas leq_card_fsetU, leq_card_coverg
- lemma trivIsetP, cover_imfset, big_trivIset
- lemma partition_disjoint_bigfcup

affeldt-aist commented 4 years ago

~Builds with Coq 8.7, 8.8, 8.9 failing.~ Problem addressed. Thanks @pi8027