mathlib3

52fa514e - feat(data/set/finite): Add lemmas relating definitions of infinite sets (#18620)

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 Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>