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.

Estimated changes