iAlls — Mathlib

English

Transform a formula by existentially quantifying over all Sum.inr variables and enforcing a uniqueness constraint for the chosen witnesses.

Русский

Применить существование карьтерам Sum.inr и потребовать единственность решения.

LaTeX

$$$\\text{iExsUnique} : [Finite\\; β] \\to (\\phi: L.Formula (α \\oplus β) \\to L.Formula α)$$$

Lean4

/-- `iAlls f φ` transforms a `L.Formula (α ⊕ β)` into a `L.Formula α` by universally
quantifying over all variables `Sum.inr _`. -/
noncomputable def iAlls [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) φ).alls

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