realize_castLE_of_eq — Mathlib

English

When m = n and h' is a valid length extension, realizing castLE preserves realization: Realize of castLE φ equals realizing φ after composing xs with the cast.

Русский

При m = n и допустимом удлинении длины h' реализация castLE сохраняет реализацию: Realize castLE φ эквивалентна реализации φ после композиции xs с cast.

LaTeX

$$$ (\phi.castLE h').Realize v xs \iff \phi.Realize v (xs \circ Fin.cast h) $$$

Lean4

theorem realize_castLE_of_eq {m n : ℕ} (h : m = n) {h' : m ≤ n} {φ : L.BoundedFormula α m} {v : α → M}
    {xs : Fin n → M} : (φ.castLE h').Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast h) :=
  by
  subst h
  simp only [castLE_rfl, cast_refl, Function.comp_id]

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