Commit 2023-12-09 13:26 818337c6

View on Github →

feat: Finsets and multisets are graded (#8892) Characterise IsAtom, IsCoatom, Covby in Set α, Multiset α, Finset α and deduce that Multiset α, Finset α are graded orders. Note I am moving some existing characterisations to here because it makes sense thematically, but I could be convinced otherwise.

Estimated changes

deleted theorem Finset.covby_cons
deleted theorem Finset.covby_insert
added theorem Finset.insert_empty
modified theorem Finset.ssubset_iff
added theorem Finset.val_strictMono
added theorem Finset.card_strictMono
added theorem Covby.card_finset
added theorem Covby.card_multiset
added theorem Finset.coe_covby_coe
added theorem Finset.coe_wcovby_coe
added theorem Finset.covby_cons
added theorem Finset.covby_insert
added theorem Finset.erase_covby
added theorem Finset.erase_wcovby
added theorem Finset.grade_eq
added theorem Finset.val_covby_val
added theorem Finset.val_wcovby_val
added theorem Finset.wcovby_insert
added theorem Multiset.covby_cons
added theorem Multiset.covby_iff
added theorem Multiset.grade_eq
added theorem Multiset.isAtom_iff
added theorem List.sublist_singleton
added theorem List.perm_rfl
added theorem List.subperm_iff
modified theorem List.subperm_singleton_iff
added theorem Multiset.cons_lt_cons
added theorem Multiset.le_singleton
added theorem Multiset.lt_singleton
modified theorem Multiset.subset_zero
added theorem Multiset.zero_ssubset
modified theorem Set.ssubset_iff_insert
added theorem IsAtom.le_iff_eq
added theorem IsCoatom.le_iff_eq
modified theorem Set.isAtom_iff
added theorem isAtom_compl
deleted theorem isAtom_iff
added theorem isAtom_iff_le_of_ge
added theorem isCoatom_compl
deleted theorem isCoatom_iff
added theorem isCoatom_iff_ge_of_le
modified theorem Set.covby_insert
modified theorem Set.wcovby_insert
modified theorem Wcovby.rfl