realize_liftAt_one_self — Mathlib

English

A specialization showing that lifting at 1 and then reindexing by castSucc yields the same Realize as casting via castSucc and then Succ.

Русский

Специализация, показывающая, что подъём на 1 и последующая переиндексация дают одинаковую реализацию как преобразование через castSucc и затем Succ.

LaTeX

$$$ (\,\phi.liftAt 1 n).Realize v xs \iff \phi.Realize v (xs \circ \text{castSucc}) $$$

Lean4

@[simp]
theorem realize_liftAt_one_self {n : ℕ} {φ : L.BoundedFormula α n} {v : α → M} {xs : Fin (n + 1) → M} :
    (φ.liftAt 1 n).Realize v xs ↔ φ.Realize v (xs ∘ castSucc) :=
  by
  rw [realize_liftAt_one (refl n), iff_eq_eq]
  refine congr rfl (congr rfl (funext fun i => ?_))
  rw [if_pos i.is_lt]

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