Mathlib Map

Theorems · Definition · logic and foundations

PSet.Func

(x : PSet.{u_1}) → x.Type → PSet.{u_1}

The underlying pre-set family of a pre-set

Defined in
Mathlib.SetTheory.ZFC.PSet
Cited by
29 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

PSet.rank_lt_of_mem · cited by 7PSet.rank_lt_of_memPSet.sUnion · cited by 5PSet.sUnionPSet.mem_insert_iff · cited by 4PSet.mem_insert_iffZFSet.mem_image · cited by 3ZFSet.mem_imagePSet.equiv_iff · cited by 3PSet.equiv_iffPSet.mem_of_subset · cited by 3PSet.mem_of_subsetZFSet.image.mk · cited by 3image.mkPSet.image · cited by 2PSet.imagePSet.mem_powerset · cited by 2PSet.mem_powersetPSet.mem_sUnion · cited by 2PSet.mem_sUnionPSet.powerset · cited by 2PSet.powersetPSet.subset_iff · cited by 2PSet.subset_iffZFSet.subset_iff · cited by 2ZFSet.subset_iffPSet.equiv_iff_mem · cited by 1PSet.equiv_iff_memPSet.eta · cited by 1PSet.etaPSet · cited by 107PSetPSet.Type · cited by 34PSet.TypePSet.FuncCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • PSetstatement and proof · cited by 107
  • PSet.Typestatement and proof · cited by 34

Cited by36

Results whose statement or proof uses this declaration.