Commit 2023-07-10 12:17 1e37d20f
View on Github →fix: fix wrong namespace for finite_iff_bdd lemmas (#5783)
This fixes an issue with my earlier PR adding three lemmas about finiteness/boundedness, which were incorrectly defined in the Finset
namespace rather than Set
.