ModelsBoundedFormula — Mathlib

English

A theory models a bounded formula if every nonempty model of the theory realizes the formula for all inputs.

Русский

Теория моделирует ограниченную формулу, если каждая ненулевой модели теории реализует формулу для всех входов.

LaTeX

$$$\\mathrm{ModelsBoundedFormula}(\\varphi) \\iff \\forall M, \\forall v, \\forall xs, \\varphi\\text{.Realize } v\, xs.$$$

Lean4

/-- A theory models a (bounded) formula when any of its nonempty models realizes that formula on all
  inputs. -/
def ModelsBoundedFormula (φ : L.BoundedFormula α n) : Prop :=
  ∀ (M : ModelType.{u, v, max u v w} T) (v : α → M) (xs : Fin n → M), φ.Realize v xs

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