Theorems · Definition · logic and foundations

ZFSet.Definable.recOn

{n : ℕ} →
  {f : (Fin n → ZFSet.{u}) → ZFSet.{u}} →
    {motive : ZFSet.Definable n f → Sort u_1} →
      (t : ZFSet.Definable n f) →
        ((out : (Fin n → PSet.{u}) → PSet.{u}) →
            (mk_out : ∀ (xs : Fin n → PSet.{u}), ZFSet.mk (out xs) = f fun x => ZFSet.mk (xs x)) →
              motive { out := out, mk_out := mk_out }) →
          motive t

Defined in

Mathlib.SetTheory.ZFC.Basic

Cited by

0 results in Mathlib

Foundations

Depth 18 from the axioms · uses no axioms