models_formula_iff — Mathlib

English

A bounded formula φ is realized in all models of T iff T.modelsBoundedFormula φ holds for all such models after an appropriate encoding.

Русский

Ограниченная формула φ реализуется во всех моделях T тогда и только тогда, когда T моделирует φ через соответствующее кодирование.

LaTeX

$$$T \\models^b φ \\iff \\forall M \\in \\text{Mod}_T: φ\\text{Realize } M.$$$

Lean4

theorem models_formula_iff {φ : L.Formula α} :
    T ⊨ᵇ φ ↔ ∀ (M : ModelType.{u, v, max u v w} T) (v : α → M), φ.Realize v :=
  forall_congr' fun _ => forall_congr' fun _ => Unique.forall_iff

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