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

Estimated changes

added theorem Finset.card_le_card
deleted theorem Finset.card_le_of_subset
deleted theorem Finset.card_lt_card
modified theorem Finset.card_mono
added theorem Finset.filter_image
deleted theorem Finset.image_filter
added theorem Multiset.card_le_card
deleted theorem Multiset.card_le_of_le
added theorem Multiset.card_lt_card
deleted theorem Multiset.card_lt_of_lt
modified theorem Multiset.card_mono
modified theorem Multiset.card_strictMono
added theorem Set.encard_le_card
deleted theorem Set.encard_le_of_subset
added theorem Set.ncard_le_ncard
deleted theorem Set.ncard_le_of_subset
modified theorem Set.ncard_mono
added theorem Set.card_le_card
deleted theorem Set.card_le_of_subset