Commit 2025-08-26 10:33 ff642c04
View on Github →feat: IsSuccLimit a → (Iio a).Nonempty (#28946)
Given that I could find multiple times this gets reproved (and Bhavik was going to add one to that list!) we might as well have this as a theorem.
feat: IsSuccLimit a → (Iio a).Nonempty (#28946)
Given that I could find multiple times this gets reproved (and Bhavik was going to add one to that list!) we might as well have this as a theorem.