Mathlib Map

Theorems · Theorem · logic and foundations

PSet.equiv_iff

∀ {x : PSet.{u_1}} {y : PSet.{u_2}},
  x.Equiv y ↔ (∀ (i : x.Type), ∃ j, (x.Func i).Equiv (y.Func j)) ∧ ∀ (j : y.Type), ∃ i, (x.Func i).Equiv (y.Func j)
Defined in
Mathlib.SetTheory.ZFC.PSet
Cited by
3 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

PSet.equiv_of_isEmpty · cited by 1PSet.equiv_of_isEmptyPSet.Equiv.exists_left · cited by 0Equiv.exists_leftPSet.Equiv.exists_right · cited by 0Equiv.exists_rightPSet · cited by 107PSetPSet.Equiv · cited by 44PSet.EquivPSet.Type · cited by 34PSet.TypePSet.Func · cited by 29PSet.FuncPSet.equiv_iffCITED BYCITES

Cites4

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.Equivstatement and proof · cited by 44
  • PSet.Typestatement and proof · cited by 34
  • PSet.Funcstatement and proof · cited by 29

Cited by3

Results whose statement or proof uses this declaration.