Theorems · Inductive type · logic and foundations

FirstOrder.Language.Hom

(L : FirstOrder.Language) → (M : Type w) → (N : Type w') → [L.Structure M] → [L.Structure N] → Type (max w w')

A homomorphism between first-order structures is a function that commutes with the interpretations of functions and maps tuples in one structure where a given relation is true to tuples in the second structure where that relation is still true.

Defined in

Mathlib.ModelTheory.Basic

Cited by

107 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 3 definitions · uses no axioms

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure