Theorems · Theorem · logic and foundations

FirstOrder.Language.isExtensionPair_iff_exists_embedding_closure_singleton_sup

∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N],
  L.IsExtensionPair M N ↔
    ∀ (S : L.Substructure M),
      S.FG → ∀ (f : L.Embedding (↥S) N) (m : M), ∃ g, f = g.comp (FirstOrder.Language.Substructure.inclusion ⋯)

An alternate characterization of an extension pair is that every finitely generated partial isomorphism can be extended to include any particular element of the domain.

Defined in

Mathlib.ModelTheory.PartialEquiv

Cited by

1 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure