realize_relabel_sumInr — Mathlib

English

Specialization of relabeling to the Sum.inr injection proves that the realization of the relabeled φ on Fin n reduces to the realization of φ on Fin n.

Русский

Специализация переименования к инъекции Sum.inr доказывает, что реализация переименованной φ на Fin n сводится к реализации φ на Fin n.

LaTeX

$$$ (\BoundedFormula.realize\_relabel)\, (\mathrm{Sum.inr}\; \varphi) \, (v) \, x \iff \varphi^M(x) $$$

Lean4

theorem realize_relabel_sumInr (φ : L.Formula (Fin n)) {v : Empty → M} {x : Fin n → M} :
    (BoundedFormula.relabel Sum.inr φ).Realize v x ↔ φ.Realize x := by
  rw [BoundedFormula.realize_relabel, Formula.Realize, Sum.elim_comp_inr, Fin.castAdd_zero, cast_refl, Function.comp_id,
    Subsingleton.elim (x ∘ (natAdd n : Fin 0 → Fin n)) default]

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