Theorems · Theorem · logic and foundations

FirstOrder.Language.IsUltrahomogeneous.extend_embedding

∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M],
  L.IsUltrahomogeneous M →
    ∀ {S : Type u_1} [inst_1 : L.Structure S],
      FirstOrder.Language.Structure.FG L S →
        ∀ {T : Type u_2} [inst_2 : L.Structure T] [h : Nonempty (L.Embedding T M)] (f : L.Embedding S M)
          (g : L.Embedding S T), ∃ f', f = f'.comp g

Any embedding from a finitely generated S to an ultrahomogeneous structure M can be extended to an embedding from any structure with an embedding to M.

Defined in

Mathlib.ModelTheory.Fraisse

Cited by

2 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureFirstOrder.Language.StructureFirstOrder.Language.StructureNonempty