Realize — Mathlib

English

Equivalence of realizations when using the symmetric form of equivSentence for formulas with constants.

Русский

Эквивалентность реализаций при использовании симметричной формы equivSentence для формул с константами.

LaTeX

$$$ (equivSentence.symm \varphi).Realize v \;\Iff\; \Sentence.Realize M \varphi $$$

Lean4

/-- A sentence can be evaluated as true or false in a structure. -/
nonrec def Realize (φ : L.Sentence) : Prop :=
  φ.Realize
    (default : _ → M)
      -- input using \|= or \vDash, but not using \models

Похожие утверждения