Theorems · Definition · logic and foundations

FirstOrder.Language.BoundedFormula.IsAtomic.casesOn

∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {motive : (a : L.BoundedFormula α n) → a.IsAtomic → Prop}
  {a : L.BoundedFormula α n} (t : a.IsAtomic),
  (∀ (t₁ t₂ : L.Term (α ⊕ Fin n)), motive (t₁.bdEqual t₂) ⋯) →
    (∀ {l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)), motive (R.boundedFormula ts) ⋯) → motive a t

Defined in

Mathlib.ModelTheory.Complexity

Cited by

2 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms