# The back and forth method and countable dense linear orders #

## Results #

Suppose `α β`

are linear orders, with `α`

countable and `β`

dense, nontrivial. Then there is an
order embedding `α ↪ β`

. If in addition `α`

is dense, nonempty, without endpoints and `β`

is
countable, without endpoints, then we can upgrade this to an order isomorphism `α ≃ β`

.

The idea for both results is to consider "partial isomorphisms", which identify a finite subset of
`α`

with a finite subset of `β`

, and prove that for any such partial isomorphism `f`

and `a : α`

, we
can extend `f`

to include `a`

in its domain.

## References #

https://en.wikipedia.org/wiki/Back-and-forth_method

## Tags #

back and forth, dense, countable, order

Suppose `α`

is a nonempty dense linear order without endpoints, and
suppose `lo`

, `hi`

, are finite subsets with all of `lo`

strictly
before `hi`

. Then there is an element of `α`

strictly between `lo`

and `hi`

.

The type of partial order isomorphisms between `α`

and `β`

defined on finite subsets.
A partial order isomorphism is encoded as a finite subset of `α × β`

, consisting
of pairs which should be identified.

## Instances For

For each `a`

, we can find a `b`

in the codomain, such that `a`

's relation to
the domain of `f`

is `b`

's relation to the image of `f`

.

Thus, if `a`

is not already in `f`

, then we can extend `f`

by sending `a`

to `b`

.

A partial isomorphism between `α`

and `β`

is also a partial isomorphism between `β`

and `α`

.

## Instances For

The set of partial isomorphisms defined at `a : α`

, together with a proof that any
partial isomorphism can be extended to one defined at `a`

.

## Instances For

The set of partial isomorphisms defined at `b : β`

, together with a proof that any
partial isomorphism can be extended to include `b`

. We prove this by symmetry.

## Instances For

Given an ideal which intersects `definedAtLeft β a`

, pick `b : β`

such that
some partial function in the ideal maps `a`

to `b`

.

## Instances For

Given an ideal which intersects `definedAtRight α b`

, pick `a : α`

such that
some partial function in the ideal maps `a`

to `b`

.

## Instances For

Any countable linear order embeds in any nontrivial dense linear order.

Any two countable dense, nonempty linear orders without endpoints are order isomorphic.