Commit 2023-12-27 09:01 7d3d6e43
View on Github →chore: Improve Finset
lemma names (#8894)
Change a few lemma names that have historically bothered me.
Finset.card_le_of_subset
→Finset.card_le_card
Multiset.card_le_of_le
→Multiset.card_le_card
Multiset.card_lt_of_lt
→Multiset.card_lt_card
Set.ncard_le_of_subset
→Set.ncard_le_ncard
Finset.image_filter
→Finset.filter_image
CompleteLattice.finset_sup_compact_of_compact
→CompleteLattice.isCompactElement_finset_sup