English
Any two countable dense, nonempty linear orders without endpoints are order-isomorphic.
Русский
Любые две счетные плотные непустые линейные порядка без точек конца взаимно изоморфны по порядку.
LaTeX
$$$\\\\exists \\\\varphi : \\\\alpha \\\\overset{\\\\mathrm{ord}}{\\\\cong} \\\\beta.$$$
Lean4
/-- Any countable linear order embeds in any nontrivial dense linear order. -/
theorem embedding_from_countable_to_dense [Countable α] [DenselyOrdered β] [Nontrivial β] : Nonempty (α ↪o β) :=
by
cases nonempty_encodable α
rcases exists_pair_lt β with ⟨x, y, hxy⟩
obtain ⟨a, ha⟩ := exists_between hxy
haveI : Nonempty (Set.Ioo x y) := ⟨⟨a, ha⟩⟩
let our_ideal : Ideal (PartialIso α _) := idealOfCofinals default (definedAtLeft (Set.Ioo x y))
let F a := funOfIdeal a our_ideal (cofinal_meets_idealOfCofinals _ _ a)
refine
⟨RelEmbedding.trans (OrderEmbedding.ofStrictMono (fun a ↦ (F a).val) fun a₁ a₂ ↦ ?_) (OrderEmbedding.subtype _)⟩
rcases (F a₁).prop with ⟨f, hf, ha₁⟩
rcases (F a₂).prop with ⟨g, hg, ha₂⟩
rcases our_ideal.directed _ hf _ hg with ⟨m, _hm, fm, gm⟩
exact (lt_iff_lt_of_cmp_eq_cmp <| m.prop (a₁, _) (fm ha₁) (a₂, _) (gm ha₂)).mp
