inf

Mathlib.ModelTheory.Complexity

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

English

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

Русский

Если φ и ψ квантитно-фри, то φ ∧ ψ квантитно-фри.

LaTeX

$$$IsQF(\varphi \sqcap \psi)$$$

Lean4

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

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

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

Разделы

Аффилиация

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