Mathlib Map

Theorems · Definition · logic and foundations

ZFSet.pair

ZFSet.{u} → ZFSet.{u} → ZFSet.{u}

Kuratowski ordered pair

Defined in
Mathlib.SetTheory.ZFC.Basic
Cited by
12 results in Mathlib
Foundations
Depth 19 from the axioms · uses Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ZFSet.map · cited by 4ZFSet.mapZFSet.IsFunc · cited by 3ZFSet.IsFuncClass.fval · cited by 3Class.fvalZFSet.pair_injective · cited by 3ZFSet.pair_injectiveZFSet.map_fval · cited by 1ZFSet.map_fvalZFSet.map_isFunc · cited by 1ZFSet.map_isFuncZFSet.map_unique · cited by 1ZFSet.map_uniqueZFSet.mem_map · cited by 1ZFSet.mem_mapZFSet.pairSep · cited by 1ZFSet.pairSepZFSet.pair_mem_prod · cited by 1ZFSet.pair_mem_prodZFSet.mem_funs · cited by 0ZFSet.mem_funsZFSet.mem_pairSep · cited by 0ZFSet.mem_pairSepZFSet.mem_prod · cited by 0ZFSet.mem_prodClass.fval_ex · cited by 0Class.fval_exZFSet.coe_pair · cited by 0ZFSet.coe_pairZFSet · cited by 259ZFSetZFSet.pairCITED BYCITES

Cites1

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

  • ZFSetstatement and proof · cited by 259

Cited by16

Results whose statement or proof uses this declaration.