mathlib3

505097f4 - feat(order): countable categoricity of dense linear orders (#2860)

feat(order): countable categoricity of dense linear orders (#2860) We construct an order isomorphism between any two countable, nonempty, dense linear orders without endpoints, using the back-and-forth method.