Countable atomless Boolean algebras are isomorphic

Any two countable, nontrivial, atomless (equivalently, densely ordered) Boolean algebras are order isomorphic (iso_of_countable_atomless).

theorem BooleanSubalgebra.coe_bot_finite {α : Type u_1} [BooleanAlgebra α] : (↑⊥).Finite

structure PartialIso (α : Type u_1) (β : Type u_2) [BooleanAlgebra α] [BooleanAlgebra β] : Type (max u_1 u_2)

A partial isomorphism between α and β: an order isomorphism between two finite Boolean subalgebras.

• domSubalg : BooleanSubalgebra α
• codSubalg : BooleanSubalgebra β
• finite_dom : (↑self.domSubalg).Finite
• finite_cod : (↑self.codSubalg).Finite
• iso : ↥self.domSubalg ≃o ↥self.codSubalg

@[instance_reducible]

instance PartialIso.instPreorder {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] : Preorder (PartialIso α β)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance PartialIso.instInhabitedOfNontrivial {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] [Nontrivial α] [Nontrivial β] : Inhabited (PartialIso α β)

Equations

• PartialIso.instInhabitedOfNontrivial = { default := { domSubalg := ⊥, codSubalg := ⊥, finite_dom := ⋯, finite_cod := ⋯, iso := botOrderIso } }

def PartialIso.comm {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] : PartialIso α β → PartialIso β α

Equations

• f.comm = { domSubalg := f.codSubalg, codSubalg := f.domSubalg, finite_dom := ⋯, finite_cod := ⋯, iso := f.iso.symm }

theorem PartialIso.le_def {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] {f g : PartialIso α β} : f ≤ g ↔ ∃ (hA : f.domSubalg ≤ g.domSubalg), ∀ (x : ↥f.domSubalg), ↑(g.iso ⟨↑x, ⋯⟩) = ↑(f.iso x)

theorem PartialIso.cod_le_of_le {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] {f g : PartialIso α β} (hfg : f ≤ g) : f.codSubalg ≤ g.codSubalg

theorem PartialIso.symm_agree_of_le {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] {f g : PartialIso α β} (hfg : f ≤ g) (v : ↥f.codSubalg) : ↑(g.iso.symm ⟨↑v, ⋯⟩) = ↑(f.iso.symm v)

theorem PartialIso.comm_le_comm {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] {f g : PartialIso α β} (hfg : f ≤ g) : f.comm ≤ g.comm

theorem PartialIso.eval_eq_of_mem_of_mem {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] {f g : PartialIso α β} {I : Order.Ideal (PartialIso α β)} (hf : f ∈ I) (hg : g ∈ I) {a : α} (haf : a ∈ f.domSubalg) (hag : a ∈ g.domSubalg) : ↑(f.iso ⟨a, haf⟩) = ↑(g.iso ⟨a, hag⟩)

theorem PartialIso.symm_eval_eq_of_mem_of_mem {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] {f g : PartialIso α β} {I : Order.Ideal (PartialIso α β)} (hf : f ∈ I) (hg : g ∈ I) {b : β} (hbf : b ∈ f.codSubalg) (hbg : b ∈ g.codSubalg) : ↑(f.iso.symm ⟨b, hbf⟩) = ↑(g.iso.symm ⟨b, hbg⟩)

theorem PartialIso.exists_le_mem_dom {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] [Nontrivial β] [DenselyOrdered β] (f : PartialIso α β) (a : α) : ∃ (g : PartialIso α β), f ≤ g ∧ a ∈ g.domSubalg

def PartialIso.definedAtLeft {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] [Nontrivial β] [DenselyOrdered β] (a : α) : Order.Cofinal (PartialIso α β)

The cofinal family of partial isomorphisms whose domain contains a.

Equations

• PartialIso.definedAtLeft a = { carrier := {f : PartialIso α β | a ∈ f.domSubalg}, isCofinal := ⋯ }

def PartialIso.definedAtRight {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] [Nontrivial α] [DenselyOrdered α] (b : β) : Order.Cofinal (PartialIso α β)

The cofinal family of partial isomorphisms whose codomain contains b.

Equations

• PartialIso.definedAtRight b = { carrier := {f : PartialIso α β | b ∈ f.codSubalg}, isCofinal := ⋯ }

theorem iso_of_countable_atomless {α : Type u_1} {β : Type u_2} [BooleanAlgebra α] [BooleanAlgebra β] [Countable α] [Nontrivial α] [DenselyOrdered α] [Countable β] [Nontrivial β] [DenselyOrdered β] : Nonempty (α ≃o β)