Commit 2024-11-03 18:36 a54ab2c4
View on Github →chore(SetTheory/Cardinal/Basic): generalize bddAbove_range
(#17025)
In truth we could simply replace all instances of bddAbove_range
with bddAbove_of_small
, but I've kept the lemma anyways for discoverability.