Theorem BddBelow.finite_of_bddAbove

Modification history

2024-02-20 17:52

Mathlib/Data/Finset/LocallyFinite/Basic.lean

chore: move BddBelow.finite_of_bddAbove to Order.LocallyFinite (#10613)

Modified BddBelow.finite_of_bddAbove View on Github →

2023-01-26 10:01

Mathlib/Data/Finset/LocallyFinite.lean

feat: port Data.Finset.LocallyFinite (#1837)

Added BddBelow.finite_of_bddAbove View on Github →