Theorems · Theorem · logic and foundations

FirstOrder.Language.equiv_between_cg

∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  FirstOrder.Language.Structure.CG L M →
    FirstOrder.Language.Structure.CG L N →
      ∀ (g : L.FGEquiv M N), L.IsExtensionPair M N → L.IsExtensionPair N M → ∃ f, ↑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.

Defined in

Mathlib.ModelTheory.PartialEquiv

Cited by

2 results in Mathlib

Foundations

Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure