sup

Mathlib.ModelTheory.Complexity

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.BoundedFormula.IsQF.sup

English

If φ and ψ are quantifier-free, then their supremum is quantifier-free.

Русский

Пусть φ и ψ — квантитно-фри формулы; их объединение (супр) также квантитно-фри.

LaTeX

$$$IsQF(\varphi \sqcup \psi)$$$

Lean4

theorem sup {φ ψ : L.BoundedFormula α n} (hφ : IsQF φ) (hψ : IsQF ψ) : IsQF (φ ⊔ ψ) :=
  hφ.not.imp hψ

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

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

Разделы

Аффилиация

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