relabel_ex — Mathlib

English

Let g be as above and φ a bounded formula. Relabeling commutes with the existential quantifier: φ.ex.relabel g = (φ.relabel g).ex.

Русский

Пусть g как выше и φ — ограниченная формула. Переименование сохраняет существование: φ.ex.relabel g = (φ.relabel g).ex.

LaTeX

$$$\\forall g:\\alpha \\to (\\beta \\oplus \\mathrm{Fin}(n))\\,\\forall k:\\mathbb{N}\\;\\; \\phi:\\,L.BoundedFormula\\,\\alpha\\,(k+1):\\; \\phi.ex.\\relabel\\ g = (\\phi.\\relabel\\ g).ex$$$

Lean4

@[simp]
theorem relabel_ex (g : α → β ⊕ (Fin n)) {k} (φ : L.BoundedFormula α (k + 1)) : φ.ex.relabel g = (φ.relabel g).ex := by
  simp [BoundedFormula.ex]

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