formula_mem_typeOf — Mathlib

English

Let L be a language, T a theory, M a model of T, and v : α → M. Then a formula φ with free variables α belongs to the complete type T.typeOf v in T if and only if φ is realized by v in M; i.e. φ.Realize v holds exactly when φ ∈ T.typeOf v.

Русский

Пусть L — язык, T — теория, M — модель T, и v : α → M. Тогда формула φ с свободными переменными α принадлежит полному типу T.typeOf v в T тогда и только тогда, когда φ реализуется на v в M; т.е. φ.Realize v эквивалентно φ ∈ T.typeOf v.

LaTeX

$$$\varphi \in T.typeOf(v) \iff \varphi.Realize(v)$$$

Lean4

theorem formula_mem_typeOf {φ : L.Formula α} : Formula.equivSentence φ ∈ T.typeOf v ↔ φ.Realize v := by simp

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