liftAt

Mathlib.ModelTheory.Complexity

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.BoundedFormula.IsPrenex.liftAt

← MathLib Explorer

English

Lifting indices preserves prenex form.

Русский

Перенос индексов сохраняет пренекс-форму.

LaTeX

$$$IsPrenex(\varphi.liftAt k m)$$$

Lean4

theorem liftAt {k m : ℕ} (h : IsPrenex φ) : (φ.liftAt k m).IsPrenex :=
  IsPrenex.recOn h (fun ih => ih.liftAt.isPrenex) (fun _ ih => ih.castLE.all) fun _ ih => ih.castLE.ex

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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