Theorems · Inductive type · logic and foundations
ZFSet.Definable
(n : ℕ) → ((Fin n → ZFSet.{u}) → ZFSet.{u}) → Type (u + 1)A set function is "definable" if it is the image of some n-ary PSet
function. This isn't exactly definability, but is useful as a sufficient
condition for functions that have a computable image.
- Defined in
- Mathlib.SetTheory.ZFC.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ZFSetstatement · cited by 259
Cited by12
Results whose statement or proof uses this declaration.
- ZFSet.Definable₁proof · cited by 10
- ZFSet.Definable.mk_outstatement and proof · cited by 3
- ZFSet.Definable₂proof · cited by 2
- ZFSet.Definable.outstatement and proof · cited by 2
- ZFSet.Definable.out_equivstatement and proof · cited by 2
- Classical.allZFSetDefinablestatement · cited by 0
- ZFSet.Definable.casesOnstatement and proof · cited by 0
- ZFSet.Definable.ctorIdxstatement and proof · cited by 0
- ZFSet.Definable.noConfusionstatement and proof · cited by 0
- ZFSet.Definable.noConfusionTypestatement and proof · cited by 0
- ZFSet.Definable.recOnstatement and proof · cited by 0
- ZFSet.Definable.mk.noConfusionstatement · cited by 0