Theorems · Theorem · logic and foundations

FirstOrder.Language.HomClass.map_rel

∀ {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 : ℕ}
  (r : L.Relations n) (x : Fin n → M),
  FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x)

The homomorphism sends related elements to related elements

Defined in

Mathlib.ModelTheory.Basic

Cited by

3 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

FirstOrder.Language.HomClass