mathlib3

3e175454 - feat(order/upper_lower/locally_finite): Upper closure preserves finiteness (#18678)

feat(order/upper_lower/locally_finite): Upper closure preserves finiteness (#18678) `locally_finite_order` and `upper_set` don't naturally impot one another, so I'm dumping those two lemmas in a new file.