Commit 2025-11-02 19:19 a6a3bc9c

feat(Set): finite cardinality iff [Finite] (#30245) Add a lemma making it easy to derive Finite α from ENat.card α < ⊤. Note that immediately above, the following three lemmas are defined:

@[simp high]
theorem card_eq_top_of_infinite [Infinite α] : card α = ⊤ := by ...
@[simp] lemma card_eq_top : card α = ⊤ ↔ Infinite α := by ...
@[simp] theorem card_lt_top_of_finite [Finite α] : card α < ⊤ := by ...

card_lt_top is the analog of card_eq_top, so symmetry implies that card_lt_top_of_finite should be marked @[simp high] and card_lt_top should be marked @[simp]. I find this use of @[simp] a bit surprising so I wanted to highlight this to reviewers.