Theorems · Theorem · logic and foundations

FirstOrder.Language.Hom.comp_assoc

∀ {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] {Q : Type u_2} [inst_3 : L.Structure Q] (f : L.Hom M N) (g : L.Hom N P) (h : L.Hom P Q),
  (h.comp g).comp f = h.comp (g.comp f)

Composition of first-order homomorphisms is associative.

Defined in

Mathlib.ModelTheory.Basic

Cited by

0 results in Mathlib

Foundations

Depth 18 from the axioms · uses no axioms

Assumes

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