# mathlibdocumentation

order.countable_dense_linear_order

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

## Results #

Suppose α β are linear orders, with α countable and β dense, nonempty, without endpoints. Then there is an order embedding α ↪ β. If in addition α is dense, nonempty, without endpoints and β is countable, 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

theorem order.exists_between_finsets {α : Type u_1} [linear_order α] [no_bot_order α] [no_top_order α] [nonem : nonempty α] (lo hi : finset α) (lo_lt_hi : ∀ (x : α), x lo∀ (y : α), y hix < y) :
∃ (m : α), (∀ (x : α), x lox < m) ∀ (y : α), y him < y

Suppose α is a nonempty dense linear order without endpoints, and suppose lo, hi, are finite subssets with all of lo strictly before hi. Then there is an element of α strictly between lo and hi.

def order.partial_iso (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] :
Type (max u_1 u_2)

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.

Equations
@[protected, instance]
def order.partial_iso.inhabited (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] :
Equations
@[protected, instance]
def order.partial_iso.preorder (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] :
Equations
theorem order.partial_iso.exists_across {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] [no_bot_order β] [no_top_order β] [nonempty β] (f : β) (a : α) :
∃ (b : β), ∀ (p : α × β), p f.valcmp p.fst a = cmp p.snd b

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.

@[protected]
noncomputable def order.partial_iso.comm {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] :

A partial isomorphism between α and β is also a partial isomorphism between β and α.

Equations
def order.partial_iso.defined_at_left {α : Type u_1} (β : Type u_2) [linear_order α] [linear_order β] [no_bot_order β] [no_top_order β] [nonempty β] (a : α) :

The set of partial isomorphisms defined at a : α, together with a proof that any partial isomorphism can be extended to one defined at a.

Equations
def order.partial_iso.defined_at_right (α : Type u_1) {β : Type u_2} [linear_order α] [linear_order β] [no_bot_order α] [no_top_order α] [nonempty α] (b : β) :

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.

Equations
noncomputable def order.partial_iso.fun_of_ideal {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] [no_bot_order β] [no_top_order β] [nonempty β] (a : α) (I : order.ideal β)) :
(∃ (f : , f I){b // ∃ (f : {f // ∀ (p q : α × β), p fq fcmp p.fst q.fst = cmp p.snd q.snd}) (H : f I), (a, b) f.val}

Given an ideal which intersects defined_at_left β a, pick b : β such that some partial function in the ideal maps a to b.

Equations
noncomputable def order.partial_iso.inv_of_ideal {α : Type u_1} {β : Type u_2} [linear_order α] [linear_order β] [no_bot_order α] [no_top_order α] [nonempty α] (b : β) (I : order.ideal β)) :
(∃ (f : , f I){a // ∃ (f : {f // ∀ (p q : α × β), p fq fcmp p.fst q.fst = cmp p.snd q.snd}) (H : f I), (a, b) f.val}

Given an ideal which intersects defined_at_right α b, pick a : α such that some partial function in the ideal maps a to b.

Equations
noncomputable def order.embedding_from_countable_to_dense (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] [encodable α] [no_bot_order β] [no_top_order β] [nonempty β] :
α ↪o β

Any countable linear order embeds in any nonempty dense linear order without endpoints.

Equations
noncomputable def order.iso_of_countable_dense (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] [encodable α] [no_bot_order α] [no_top_order α] [nonempty α] [encodable β] [no_bot_order β] [no_top_order β] [nonempty β] :
α ≃o β

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

Equations
• = let to_cofinal : α β := λ (p : α β), p.rec_on , our_ideal : := to_cofinal, F : Π (a : α), {b // ∃ (f : {f // ∀ (p q : α × β), p fq fcmp p.fst q.fst = cmp p.snd q.snd}) (H : f our_ideal), (a, b) f.val} := λ (a : α), our_ideal _, G : Π (b : β), {a // ∃ (f : {f // ∀ (p q : α × β), p fq fcmp p.fst q.fst = cmp p.snd q.snd}) (H : f our_ideal), (a, b) f.val} := λ (b : β), our_ideal _ in order_iso.of_cmp_eq_cmp (λ (a : α), (F a).val) (λ (b : β), (G b).val) _