Theorems · Theorem · logic and foundations

FirstOrder.Language.HomClass.map_fun

∀ {L : outParam FirstOrder.Language} {F : Type u_3} {M : outParam (Type u_4)} {N : outParam (Type u_5)}
  {inst : FunLike F M N} {inst_1 : L.Structure M} {inst_2 : L.Structure N} [self : L.HomClass F M N] (φ : F) {n : ℕ}
  (f : L.Functions n) (x : Fin n → M),
  φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)

The homomorphism commutes with the interpretations of the function symbols

Defined in

Mathlib.ModelTheory.Basic

Cited by

6 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

FirstOrder.Language.HomClass