Partial Isomorphisms #

This file defines partial isomorphisms between first-order structures.

Main Definitions #

FirstOrder.Language.PartialEquiv is defined so that L.PartialEquiv M N, annotated M ≃ₚ[L] N, is the type of equivalences between substructures of M and N.

structure FirstOrder.Language.PartialEquiv (L : FirstOrder.Language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] :

Type (max w w')

A partial L-equivalence, implemented as an equivalence between substructures.

dom : L.Substructure M
The substructure which is the domain of the equivalence.
cod : L.Substructure N
The substructure which is the codomain of the equivalence.
toEquiv : L.Equiv ↥self.dom ↥self.cod
The equivalence between the two subdomains.

Instances For

source

def FirstOrder.«term_≃ₚ[_]_» :

Lean.TrailingParserDescr

A partial L-equivalence, implemented as an equivalence between substructures.

Equations

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

Instances For

source

noncomputable instance FirstOrder.Language.PartialEquiv.instInhabited_self {L : FirstOrder.Language} {M : Type w} [L.Structure M] :

Inhabited (L.PartialEquiv M M)

Equations

FirstOrder.Language.PartialEquiv.instInhabited_self = { default := { dom := ⊤, cod := ⊤, toEquiv := FirstOrder.Language.Equiv.refl L ↥⊤ } }

source

def FirstOrder.Language.PartialEquiv.symm {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) :

L.PartialEquiv N M

Maps to the symmetric partial equivalence.

Equations

f.symm = { dom := f.cod, cod := f.dom, toEquiv := f.toEquiv.symm }

Instances For

source

@[simp]

theorem FirstOrder.Language.PartialEquiv.symm_symm {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) :

f.symm.symm = f

source

@[simp]

theorem FirstOrder.Language.PartialEquiv.symm_apply {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) (x : ↥f.cod) :

f.symm.toEquiv x = f.toEquiv.symm x

source

instance FirstOrder.Language.PartialEquiv.instLE {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :

LE (L.PartialEquiv M N)

Equations

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

source

theorem FirstOrder.Language.PartialEquiv.le_def {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) (g : L.PartialEquiv M N) :

f ≤ g ↔ ∃ (h : f.dom ≤ g.dom), g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (FirstOrder.Language.Substructure.inclusion h)) = f.cod.subtype.comp f.toEquiv.toEmbedding

source

theorem FirstOrder.Language.PartialEquiv.dom_le_dom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} :

f ≤ g → f.dom ≤ g.dom

source

theorem FirstOrder.Language.PartialEquiv.cod_le_cod {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} :

f ≤ g → f.cod ≤ g.cod

source

theorem FirstOrder.Language.PartialEquiv.subtype_toEquiv_inclusion {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} (h : f ≤ g) :

g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (FirstOrder.Language.Substructure.inclusion ⋯)) = f.cod.subtype.comp f.toEquiv.toEmbedding

source

theorem FirstOrder.Language.PartialEquiv.toEquiv_inclusion {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} (h : f ≤ g) :

g.toEquiv.toEmbedding.comp (FirstOrder.Language.Substructure.inclusion ⋯) = (FirstOrder.Language.Substructure.inclusion ⋯).comp f.toEquiv.toEmbedding

source

theorem FirstOrder.Language.PartialEquiv.toEquiv_inclusion_apply {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} (h : f ≤ g) (x : ↥f.dom) :

g.toEquiv ((FirstOrder.Language.Substructure.inclusion ⋯) x) = (FirstOrder.Language.Substructure.inclusion ⋯) (f.toEquiv x)

source

theorem FirstOrder.Language.PartialEquiv.le_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} :

f ≤ g ↔ ∃ (dom_le_dom : f.dom ≤ g.dom) (cod_le_cod : f.cod ≤ g.cod), ∀ (x : ↥f.dom), (FirstOrder.Language.Substructure.inclusion cod_le_cod) (f.toEquiv x) = g.toEquiv ((FirstOrder.Language.Substructure.inclusion dom_le_dom) x)

source

theorem FirstOrder.Language.PartialEquiv.le_trans {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) (g : L.PartialEquiv M N) (h : L.PartialEquiv M N) :

f ≤ g → g ≤ h → f ≤ h

source

instance FirstOrder.Language.PartialEquiv.instPartialOrder {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :

PartialOrder (L.PartialEquiv M N)

Equations

FirstOrder.Language.PartialEquiv.instPartialOrder = PartialOrder.mk ⋯

source

theorem FirstOrder.Language.PartialEquiv.symm_le_symm {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} (hfg : f ≤ g) :

f.symm ≤ g.symm

source

theorem FirstOrder.Language.PartialEquiv.monotone_symm {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :

Monotone fun (f : L.PartialEquiv M N) => f.symm

source

theorem FirstOrder.Language.PartialEquiv.symm_le_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv N M} :

f.symm ≤ g ↔ f ≤ g.symm

source

theorem FirstOrder.Language.PartialEquiv.ext {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} (h_dom : f.dom = g.dom) :

(∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)) → f = g

source

theorem FirstOrder.Language.PartialEquiv.ext_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} {g : L.PartialEquiv M N} :

f = g ↔ ∃ (h_dom : f.dom = g.dom), ∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)

source

theorem FirstOrder.Language.PartialEquiv.monotone_dom {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :

Monotone fun (f : L.PartialEquiv M N) => f.dom

source

theorem FirstOrder.Language.PartialEquiv.monotone_cod {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :

Monotone fun (f : L.PartialEquiv M N) => f.cod

source

noncomputable def FirstOrder.Language.PartialEquiv.domRestrict {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) {A : L.Substructure M} (h : A ≤ f.dom) :

L.PartialEquiv M N

Restriction of a partial equivalence to a substructure of the domain.

Equations

f.domRestrict h = let g := f.cod.subtype.comp (f.toEquiv.toEmbedding.comp (FirstOrder.Language.Substructure.inclusion h)); { dom := A, cod := g.toHom.range, toEquiv := g.equivRange }

Instances For

source

theorem FirstOrder.Language.PartialEquiv.domRestrict_le {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) {A : L.Substructure M} (h : A ≤ f.dom) :

f.domRestrict h ≤ f

source

theorem FirstOrder.Language.PartialEquiv.le_domRestrict {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) (g : L.PartialEquiv M N) {A : L.Substructure M} (hf : f.dom ≤ A) (hg : A ≤ g.dom) (hfg : f ≤ g) :

f ≤ g.domRestrict hg

source

noncomputable def FirstOrder.Language.PartialEquiv.codRestrict {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) {A : L.Substructure N} (h : A ≤ f.cod) :

L.PartialEquiv M N

Restriction of a partial equivalence to a substructure of the codomain.

Equations

f.codRestrict h = (f.symm.domRestrict h).symm

Instances For

source

theorem FirstOrder.Language.PartialEquiv.codRestrict_le {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) {A : L.Substructure N} (h : A ≤ f.cod) :

f.codRestrict h ≤ f

source

theorem FirstOrder.Language.PartialEquiv.le_codRestrict {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) (g : L.PartialEquiv M N) {A : L.Substructure N} (hf : f.cod ≤ A) (hg : A ≤ g.cod) (hfg : f ≤ g) :

f ≤ g.codRestrict hg

source

def FirstOrder.Language.PartialEquiv.toEmbedding {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.PartialEquiv M N) :

L.Embedding (↥f.dom) N

A partial equivalence as an embedding from its domain.

Equations

f.toEmbedding = f.cod.subtype.comp f.toEquiv.toEmbedding

Instances For

source

@[simp]

theorem FirstOrder.Language.PartialEquiv.toEmbedding_apply {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} (m : ↥f.dom) :

f.toEmbedding m = ↑(f.toEquiv m)

source

def FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} (h : f.dom = ⊤) :

L.Embedding M N

Given a partial equivalence which has the whole structure as domain, returns the corresponding embedding.

Equations

FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop h = (h ▸ f.toEmbedding).comp FirstOrder.Language.Substructure.topEquiv.symm.toEmbedding

Instances For

source

@[simp]

theorem FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop__apply {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} (h : f.dom = ⊤) (m : M) :

(FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop h) m = ↑(f.toEquiv ⟨m, ⋯⟩)

source

def FirstOrder.Language.PartialEquiv.toEquivOfEqTop {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} (h_dom : f.dom = ⊤) (h_cod : f.cod = ⊤) :

L.Equiv M N

Given a partial equivalence which has the whole structure as domain and as codomain, returns the corresponding equivalence.

Equations

FirstOrder.Language.PartialEquiv.toEquivOfEqTop h_dom h_cod = FirstOrder.Language.Substructure.topEquiv.comp ((h_dom ▸ h_cod ▸ f.toEquiv).comp FirstOrder.Language.Substructure.topEquiv.symm)

Instances For

source

@[simp]

theorem FirstOrder.Language.PartialEquiv.toEquivOfEqTop_toEmbedding {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} (h_dom : f.dom = ⊤) (h_cod : f.cod = ⊤) :

(FirstOrder.Language.PartialEquiv.toEquivOfEqTop h_dom h_cod).toEmbedding = FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop h_dom

source

theorem FirstOrder.Language.PartialEquiv.dom_fg_iff_cod_fg {L : FirstOrder.Language} {M : Type w} [L.Structure M] {N : Type u_2} [L.Structure N] (f : L.PartialEquiv M N) :

f.dom.FG ↔ f.cod.FG

source

noncomputable def FirstOrder.Language.Embedding.toPartialEquiv {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Embedding M N) :

L.PartialEquiv M N

Given an embedding, returns the corresponding partial equivalence with ⊤ as domain.

Equations

f.toPartialEquiv = { dom := ⊤, cod := f.toHom.range, toEquiv := f.equivRange.comp FirstOrder.Language.Substructure.topEquiv }

Instances For

source

theorem FirstOrder.Language.Embedding.toPartialEquiv_injective {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :

Function.Injective fun (f : L.Embedding M N) => f.toPartialEquiv

source

@[simp]

theorem FirstOrder.Language.Embedding.toEmbedding_toPartialEquiv {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Embedding M N) :

FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop ⋯ = f

source

@[simp]

theorem FirstOrder.Language.Embedding.toPartialEquiv_toEmbedding {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {f : L.PartialEquiv M N} (h : f.dom = ⊤) :

(FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop h).toPartialEquiv = f

source

instance FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureDomCoeOrderHomPartialEquivEmbeddingInclusion {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_2} [Preorder ι] (S : ι →o L.PartialEquiv M N) :

DirectedSystem (fun (i : ι) => ↥(S i).dom) fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(FirstOrder.Language.Substructure.inclusion ⋯)

Equations

⋯ = ⋯

source

instance FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureCodCoeOrderHomPartialEquivEmbeddingInclusion {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_2} [Preorder ι] (S : ι →o L.PartialEquiv M N) :

DirectedSystem (fun (i : ι) => ↥(S i).cod) fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(FirstOrder.Language.Substructure.inclusion ⋯)

Equations

⋯ = ⋯

source

noncomputable def FirstOrder.Language.DirectLimit.partialEquivLimit {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_2} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] (S : ι →o L.PartialEquiv M N) :

L.PartialEquiv M N

The limit of a directed system of PartialEquivs.

Equations

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

Instances For

source

@[simp]

theorem FirstOrder.Language.DirectLimit.dom_partialEquivLimit {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_2} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] (S : ι →o L.PartialEquiv M N) :

(FirstOrder.Language.DirectLimit.partialEquivLimit S).dom = ⨆ (x : ι), (S x).dom

source

@[simp]

theorem FirstOrder.Language.DirectLimit.cod_partialEquivLimit {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_2} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] (S : ι →o L.PartialEquiv M N) :

(FirstOrder.Language.DirectLimit.partialEquivLimit S).cod = ⨆ (x : ι), (S x).cod

source

@[simp]

theorem FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_2} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] (S : ι →o L.PartialEquiv M N) {i : ι} :

(FirstOrder.Language.DirectLimit.partialEquivLimit S).toEquiv.toEmbedding.comp (FirstOrder.Language.Substructure.inclusion ⋯) = (FirstOrder.Language.Substructure.inclusion ⋯).comp (S i).toEquiv.toEmbedding

source

theorem FirstOrder.Language.DirectLimit.le_partialEquivLimit {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {ι : Type u_2} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x x_1 : ι) => x ≤ x_1] (S : ι →o L.PartialEquiv M N) (i : ι) :

S i ≤ FirstOrder.Language.DirectLimit.partialEquivLimit S

source

@[reducible, inline]

abbrev FirstOrder.Language.FGEquiv (L : FirstOrder.Language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] :

Type (max 0 w w')

The type of equivalences between finitely generated substructures.

Equations

L.FGEquiv M N = { f : L.PartialEquiv M N // f.dom.FG }

Instances For

source

def FirstOrder.Language.IsExtensionPair (L : FirstOrder.Language) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] :

Prop

Two structures M and N form an extension pair if the domain of any finitely-generated map from M to N can be extended to include any element of M.

Equations

L.IsExtensionPair M N = ∀ (f : L.FGEquiv M N) (m : M), ∃ (g : L.FGEquiv M N), m ∈ (↑g).dom ∧ f ≤ g

Instances For

source

theorem FirstOrder.Language.countable_self_fgequiv_of_countable {L : FirstOrder.Language} {M : Type w} [L.Structure M] [Countable M] :

Countable (L.FGEquiv M M)

source

instance FirstOrder.Language.inhabited_self_FGEquiv {L : FirstOrder.Language} {M : Type w} [L.Structure M] :

Inhabited (L.FGEquiv M M)

Equations

FirstOrder.Language.inhabited_self_FGEquiv = { default := ⟨{ dom := ⊥, cod := ⊥, toEquiv := FirstOrder.Language.Equiv.refl L ↥⊥ }, ⋯⟩ }

source

@[simp]

theorem FirstOrder.Language.FGEquiv.symm_coe {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.FGEquiv M N) :

↑f.symm = (↑f).symm

source

def FirstOrder.Language.FGEquiv.symm {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.FGEquiv M N) :

L.FGEquiv N M

Maps to the symmetric finitely-generated partial equivalence.

Equations

f.symm = ⟨(↑f).symm, ⋯⟩

Instances For

source

theorem FirstOrder.Language.IsExtensionPair_iff_cod {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :

L.IsExtensionPair M N ↔ ∀ (f : L.FGEquiv N M) (m : M), ∃ (g : L.FGEquiv N M), m ∈ (↑g).cod ∧ f ≤ g

source

theorem FirstOrder.Language.IsExtensionPair.cod {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] :

L.IsExtensionPair M N → ∀ (f : L.FGEquiv N M) (m : M), ∃ (g : L.FGEquiv N M), m ∈ (↑g).cod ∧ f ≤ g

Alias of the forward direction of FirstOrder.Language.IsExtensionPair_iff_cod.

source

def FirstOrder.Language.IsExtensionPair.definedAtLeft {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (h : L.IsExtensionPair M N) (m : M) :

Order.Cofinal (L.FGEquiv M N)

The cofinal set of finite equivalences with a given element in their domain.

Equations

h.definedAtLeft m = { carrier := {f : L.FGEquiv M N | m ∈ (↑f).dom}, mem_gt := ⋯ }

Instances For

source

def FirstOrder.Language.IsExtensionPair.definedAtRight {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (h : L.IsExtensionPair N M) (n : N) :

Order.Cofinal (L.FGEquiv M N)

The cofinal set of finite equivalences with a given element in their codomain.

Equations

h.definedAtRight n = { carrier := {f : L.FGEquiv M N | n ∈ (↑f).cod}, mem_gt := ⋯ }

Instances For

source

theorem FirstOrder.Language.embedding_from_cg {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (M_cg : FirstOrder.Language.Structure.CG L M) (g : L.FGEquiv M N) (H : L.IsExtensionPair M N) :

∃ (f : L.Embedding M N), ↑g ≤ f.toPartialEquiv

For a countably generated structure M and a structure N, if any partial equivalence between finitely generated substructures can be extended to any element in the domain, then there exists an embedding of M in N.

source

theorem FirstOrder.Language.equiv_between_cg {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (M_cg : FirstOrder.Language.Structure.CG L M) (N_cg : FirstOrder.Language.Structure.CG L N) (g : L.FGEquiv M N) (ext_dom : L.IsExtensionPair M N) (ext_cod : L.IsExtensionPair N M) :

∃ (f : L.Equiv M N), ↑g ≤ f.toEmbedding.toPartialEquiv

For two countably generated structure M and N, if any PartialEquiv between finitely generated substructures can be extended to any element in the domain and to any element in the codomain, then there exists an equivalence between M and N.

Documentation

Mathlib.ModelTheory.PartialEquiv

Partial Isomorphisms #

Main Definitions #