Theorems · Theorem · logic and foundations

FirstOrder.Language.Prestructure.fun_equiv

∀ {L : FirstOrder.Language} {M : Type u_1} {s : Setoid M} [self : L.Prestructure s] {n : ℕ} {f : L.Functions n}
  (x y : Fin n → M), x ≈ y → FirstOrder.Language.Structure.funMap f x ≈ FirstOrder.Language.Structure.funMap f y

Defined in

Mathlib.ModelTheory.Quotients

Cited by

1 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

FirstOrder.Language.Prestructure