mathlib

12ee59fa - feat(data/{finset,multiset}/locally_finite): When an `Icc` is a singleton, cardinality generalization (#10925)

feat(data/{finset,multiset}/locally_finite): When an `Icc` is a singleton, cardinality generalization (#10925) This proves `Icc a b = {c} ↔ a = c ∧ b = c` for sets and finsets, gets rid of the `a ≤ b` assumption in `card_Ico_eq_card_Icc_sub_one` and friends and proves them for multisets.