isUniversal

Mathlib.ModelTheory.Complexity

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.BoundedFormula.IsAtomic.isUniversal

English

An atomic bounded formula is universal.

Русский

Атомарная ограниченная формула является универсальной.

LaTeX

$$$\forall \varphi:\ L.BoundedFormula\alpha\,n, \text{IsAtomic}(\varphi) \to \text{IsUniversal}(\varphi)$$

Lean4

theorem isUniversal {φ : L.BoundedFormula α n} (h : IsAtomic φ) : IsUniversal φ :=
  h.isQF.isUniversal

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

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

Разделы

Аффилиация

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