Theorems · Theorem · logic and foundations

FirstOrder.Language.Prestructure.rel_equiv

∀ {L : FirstOrder.Language} {M : Type u_1} {s : Setoid M} [self : L.Prestructure s] {n : ℕ} {r : L.Relations n}
  (x y : Fin n → M), x ≈ y → FirstOrder.Language.Structure.RelMap r x = FirstOrder.Language.Structure.RelMap r 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