Theorems · Definition · logic and foundations

FirstOrder.Language.BoundedFormula.brecOn

{L : FirstOrder.Language} →
  {α : Type u'} →
    {motive : (a : ℕ) → L.BoundedFormula α a → Sort u_1} →
      {a : ℕ} →
        (t : L.BoundedFormula α a) →
          ((a : ℕ) → (t : L.BoundedFormula α a) → FirstOrder.Language.BoundedFormula.below t → motive a t) → motive a t

Defined in

Mathlib.ModelTheory.Syntax

Cited by

1 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms