Theorems · Theorem · logic and foundations

FirstOrder.Language.Formula.realize_equal

∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {t₁ t₂ : L.Term α} {x : α → M},
  (t₁.equal t₂).Realize x ↔ FirstOrder.Language.Term.realize x t₁ = FirstOrder.Language.Term.realize x t₂

Defined in

Mathlib.ModelTheory.Semantics

Cited by

0 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.Structure