isQF

Mathlib.ModelTheory.Complexity

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Relations.isQF

English

A relation formula of arity l with bounded terms is quantifier-free.

Русский

ФормаRelation arity l с ограниченными термами — безкванторная.

LaTeX

$$$(r.boundedFormula ts).IsQF$$$

Lean4

theorem isQF (r : L.Relations l) (ts : Fin l → L.Term (α ⊕ (Fin n))) : IsQF (r.boundedFormula ts) :=
  (r.isAtomic ts).isQF

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru