Theorems · Definition · logic and foundations

FirstOrder.Language.Formula.iExsUnique

{L : FirstOrder.Language} → {α : Type u'} → (β : Type v') → [Finite β] → L.Formula (α ⊕ β) → L.Formula α

iExsUnique f φ transforms a L.Formula (α ⊕ β) into a L.Formula α by existentially quantifying over all variables Sum.inr _ and asserting that the solution should be unique

Defined in

Mathlib.ModelTheory.Syntax

Cited by

2 results in Mathlib

Foundations

Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Finite