Lean4
/-- A model-theoretic adaptation of the proof of `Order.iso_of_countable_dense`: two countable,
dense, nonempty linear orders without endpoints are order isomorphic. -/
example (α β : Type w') [LinearOrder α] [LinearOrder β] [Countable α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α]
[Nonempty α] [Countable β] [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β] [Nonempty β] : Nonempty (α ≃o β) :=
by
letI := orderStructure α
letI := orderStructure β
letI := StrongHomClass.toOrderIsoClass Language.order α β (α ≃[Language.order] β)
exact
⟨(IsFraisseLimit.nonempty_equiv (isFraisseLimit_of_countable_nonempty_dlo α)
(isFraisseLimit_of_countable_nonempty_dlo β)).some⟩
