Theorems · Theorem · order theory

Order.iso_of_countable_dense

• 1000+ list: Cantor's isomorphism theorem

∀ (α : Type u_1) (β : Type u_2) [inst : LinearOrder α] [inst_1 : LinearOrder β] [Countable α] [DenselyOrdered α]
  [NoMinOrder α] [NoMaxOrder α] [Nonempty α] [Countable β] [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β]
  [Nonempty β], Nonempty (α ≃o β)

Any two countable dense, nonempty linear orders without endpoints are order isomorphic. This is also known as Cantor's isomorphism theorem.

Defined in

Mathlib.Order.CountableDenseLinearOrder

Cited by

0 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderLinearOrderCountableDenselyOrderedNoMinOrderNoMaxOrderNonemptyCountableDenselyOrderedNoMinOrderNoMaxOrderNonempty