Theorems · Definition · logic and foundations

ZFSet.Definable.noConfusion

{P : Sort u_1} →
  {n : ℕ} →
    {f : (Fin n → ZFSet.{u}) → ZFSet.{u}} →
      {t : ZFSet.Definable n f} →
        {n' : ℕ} →
          {f' : (Fin n' → ZFSet.{u}) → ZFSet.{u}} →
            {t' : ZFSet.Definable n' f'} → n = n' → f ≍ f' → t ≍ t' → ZFSet.Definable.noConfusionType P t t'

Defined in

Mathlib.SetTheory.ZFC.Basic

Cited by

0 results in Mathlib

Foundations

Depth 20 from the axioms · uses no axioms