isPrenex

Mathlib.ModelTheory.Complexity

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

English

Atomic formulas are in prenex form.

Русский

атомарные формулы в пренексной форме.

LaTeX

$$$IsAtomic(\varphi) \rightarrow IsPrenex(\varphi)$$$

Lean4

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

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

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

Разделы

Аффилиация

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