mathlib

957fa4bb - feat(order/locally_finite): `with_top α`/`with_bot α` are locally finite orders (#10202)

feat(order/locally_finite): `with_top α`/`with_bot α` are locally finite orders (#10202) This provides the two instances `locally_finite_order (with_top α)` and `locally_finite_order (with_bot α)`. Co-authored-by: Adam Topaz <github@adamtopaz.com>