Commit 2023-04-25 23:03 52fa514e

feat(data/set/finite): Add lemmas relating definitions of infinite sets (#18620) Prove the following lemmas (and their dual)

• set.infinite_of_forall_exists_lt: (∀ a, ∃ b ∈ s, a < b) → s.infinite in a nonempty preorder
• set.infinite_iff_exists_lt: (∀ a, ∃ b ∈ s, a < b) ↔ s.infinite in a locally finite order with a bottom element