Theorems · Definition · logic and foundations

FirstOrder.Language.StrongHomClass.toEmbedding

{L : FirstOrder.Language} →
  {F : Type u_3} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : L.Structure M] →
          [inst_1 : L.Structure N] →
            [inst_2 : FunLike F M N] → [EmbeddingLike F M N] → [L.StrongHomClass F M N] → F → L.Embedding M N

Any element of an injective StrongHomClass can be realized as a first order embedding.

Defined in

Mathlib.ModelTheory.Basic

Cited by

4 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

FirstOrder.Language.StructureFirstOrder.Language.StructureFunLikeEmbeddingLikeFirstOrder.Language.StrongHomClass