iExs — Mathlib

English

Existentially quantify over a finite β to reduce a formula with α ⊕ β to a formula in α by relabeling and existential quantification.

Русский

Экзистенциально квантировать по β, чтобы получить формулу только по α через переименование и существование.

LaTeX

$$$[Finite\\; β] \\; (φ: L.Formula (α \\oplus β)) \\to L.Formula α$$$

Lean4

/-- `iExs f φ` transforms a `L.Formula (α ⊕ β)` into a `L.Formula α` by existentially
quantifying over all variables `Sum.inr _`. -/
noncomputable def iExs [Finite β] (φ : L.Formula (α ⊕ β)) : L.Formula α :=
  let e := Classical.choice (Classical.choose_spec (Finite.exists_equiv_fin β))
  (BoundedFormula.relabel (fun a => Sum.map id e a) φ).exs

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