Theorems · Theorem · logic and foundations

FirstOrder.Language.embedding_from_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 → ∀ (g : L.FGEquiv M N), L.IsExtensionPair M N → ∃ f, ↑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.

Defined in

Mathlib.ModelTheory.PartialEquiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure