isAtomic

Mathlib.ModelTheory.Complexity

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

English

A relation formula with a bounded tuple of terms is atomic.

Русский

Формула отношения с ограниченной кортеж-термами атомарна.

LaTeX

$$$(r).boundedFormula(ts) \text{ is atomic}$$$

Lean4

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

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

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

Разделы

Аффилиация

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