Theorems · Inductive type · logic and foundations

FirstOrder.Language.HomClass

(L : outParam FirstOrder.Language) →
  (F : Type u_3) →
    (M : outParam (Type u_4)) → (N : outParam (Type u_5)) → [FunLike F M N] → [L.Structure M] → [L.Structure N] → Prop

HomClass L F M N states that F is a type of L-homomorphisms. You should extend this typeclass when you extend FirstOrder.Language.Hom.

Defined in

Mathlib.ModelTheory.Basic

Cited by

10 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

FunLikeFirstOrder.Language.StructureFirstOrder.Language.Structure