Theorems · Theorem · logic and foundations

FirstOrder.Language.ElementaryEmbedding.map_rel

∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (φ : L.ElementaryEmbedding 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.ElementaryMaps

Cited by

0 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure