mem_typeOf — Mathlib

English

Membership of φ in T.typeOf v is equivalent to realizing the corresponding sentence under an appropriate constants-on-v structure.

Русский

Членство формулы φ в T.typeOf v эквивалентно тому, что соответствующее предложение реализуется при заданной структуре констант на v.

LaTeX

$$$\\varphi \\in T.typeOf\\ v \\iff (Formula.equivSentence.\\mathrm{symm}\\ \\varphi).Realize\\ v$$$

Lean4

@[simp]
theorem mem_typeOf {φ : L[[α]].Sentence} : φ ∈ T.typeOf v ↔ (Formula.equivSentence.symm φ).Realize v :=
  letI : (constantsOn α).Structure M := constantsOn.structure v
  mem_completeTheory.trans (Formula.realize_equivSentence_symm _ _ _).symm

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