Theorems · Theorem · logic and foundations

FirstOrder.Language.Equiv.map_fun

∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] (φ : L.Equiv M N)
  {n : ℕ} (f : L.Functions n) (x : Fin n → M),
  φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)

Defined in

Mathlib.ModelTheory.Basic

Cited by

0 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure