realize_liftAt_one — Mathlib

English

In the one-step lift,Realize of liftAt with 1 is equivalent to Realize of φ with xs adjusted by a simple conditional depending on m.

Русский

В одношаговом подъёме Realize liftAt с 1 эквивалентно реализации φ со скорректированным xs по простому условию от m.

LaTeX

$$$ (\phi.liftAt 1 m).Realize v xs \iff \phi.Realize v (xs \circ \lambda i. if \; \uparrow i < m \text{ then } castSucc i \; else \; i.succ) $$$

Lean4

theorem realize_liftAt_one {n m : ℕ} {φ : L.BoundedFormula α n} {v : α → M} {xs : Fin (n + 1) → M} (hmn : m ≤ n) :
    (φ.liftAt 1 m).Realize v xs ↔ φ.Realize v (xs ∘ fun i => if ↑i < m then castSucc i else i.succ) := by
  simp [realize_liftAt (add_le_add_right hmn 1), castSucc]

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