Theorems · Definition · logic and foundations

FirstOrder.Language.Embedding.comp

{L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          {P : Type u_1} → [inst_2 : L.Structure P] → L.Embedding N P → L.Embedding M N → L.Embedding M P

Composition of first-order embeddings.

Defined in

Mathlib.ModelTheory.Basic

Cited by

38 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound

Assumes

FirstOrder.Language.StructureFirstOrder.Language.StructureFirstOrder.Language.Structure