English
Same fundamental fact as Cantor’s isomorphism theorem, stated with explicit hypotheses on α and β.
Русский
Та же основная идея теоремы изоморфности Кантора, сформулированная с явными предпосылками на \u03b1 и \u03b2.
LaTeX
$$$\\\\exists \\\\varphi : \\\\alpha \\\\overset{\\\\mathrm{ord}}{\\\\cong} \\\\beta.$$$
Lean4
/-- Any two countable dense, nonempty linear orders without endpoints are order isomorphic. This is
also known as **Cantor's isomorphism theorem**. -/
theorem iso_of_countable_dense [Countable α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] [Nonempty α] [Countable β]
[DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β] [Nonempty β] : Nonempty (α ≃o β) :=
by
cases nonempty_encodable α
cases nonempty_encodable β
let to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p ↦ Sum.recOn p (definedAtLeft β) (definedAtRight α)
let our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
let F a := funOfIdeal a our_ideal (cofinal_meets_idealOfCofinals _ to_cofinal (Sum.inl a))
let G b := invOfIdeal b our_ideal (cofinal_meets_idealOfCofinals _ to_cofinal (Sum.inr b))
exact
⟨OrderIso.ofCmpEqCmp (fun a ↦ (F a).val) (fun b ↦ (G b).val) fun a b ↦
by
rcases (F a).prop with ⟨f, hf, ha⟩
rcases (G b).prop with ⟨g, hg, hb⟩
rcases our_ideal.directed _ hf _ hg with ⟨m, _, fm, gm⟩
exact m.prop (a, _) (fm ha) (_, b) (gm hb)⟩
