mathlib

c55911f6 - chore(order/atoms): split out finiteness results (#17866)