Theorems · Theorem · logic and foundations

FirstOrder.Language.Hom.map_rel

∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] (φ : L.Hom M N)
  {n : ℕ} (r : L.Relations n) (x : Fin n → M),
  FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x)

Defined in

Mathlib.ModelTheory.Basic

Cited by

0 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure