Theorems · Theorem · logic and foundations

FirstOrder.Language.StrongHomClass.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.StrongHomClass 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

5 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

FirstOrder.Language.StrongHomClass