Commit 2020-11-03 21:30 505097f4

View on Github →

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.

Estimated changes

Modified src/algebra/order.lean

added theorem cmp_eq_cmp_symm

added theorem cmp_eq_eq_iff

added theorem cmp_eq_gt_iff

added theorem cmp_eq_lt_iff

added theorem cmp_self_eq_eq

added theorem le_iff_le_of_cmp_eq_cmp

added theorem lt_iff_lt_of_cmp_eq_cmp

Created src/order/countable_dense_linear_order.lean

added def order.embedding_from_countable_to_dense

added theorem order.exists_between_finsets

added def order.iso_of_countable_dense

added def order.partial_iso.defined_at_left

added def order.partial_iso.defined_at_right

added theorem order.partial_iso.exists_across

added def order.partial_iso.fun_of_ideal

added def order.partial_iso.inv_of_ideal

added def order.partial_iso

Modified src/order/rel_iso.lean

added def order_embedding.of_strict_mono

added def order_iso.of_cmp_eq_cmp