Theorems · Definition · logic and foundations

FirstOrder.Language.HomClass.toHom

{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] → [L.HomClass F M N] → F → L.Hom M N

Any element of a HomClass can be realized as a first order homomorphism.

Defined in

Mathlib.ModelTheory.Basic

Cited by

1 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

FirstOrder.Language.StructureFirstOrder.Language.StructureFunLikeFirstOrder.Language.HomClass