Mathlib Map

Theorems · Definition · logic and foundations

Equiv.prodPUnit

(α : Type u_9) → α × PUnit.{u_10 + 1} ≃ α

PUnit is a right identity for type product up to an equivalence.

Defined in
Mathlib.Logic.Equiv.Prod
Cited by
2 results in Mathlib
Foundations
Depth 10 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Equiv.punitProd · cited by 9Equiv.punitProdAlgebraicGeometry.Scheme.Pullback.openCoverOfBase · cited by 6Pullback.openCoverOfBaseEquiv.prodUnique · cited by 6Equiv.prodUniqueHomeomorph.prodPUnit · cited by 2Homeomorph.prodPUnitUniformEquiv.prodPUnit · cited by 1UniformEquiv.prodPUnitField.Emb.Cardinal.equivSucc · cited by 1Cardinal.equivSuccEquiv.prodPUnit_apply · cited by 0Equiv.prodPUnit_applyEquiv.prodPUnit_symm_apply · cited by 0Equiv.prodPUnit_symm_applyMeasurableEquiv.prodPUnit · cited by 0MeasurableEquiv.prodPUnitEquiv · cited by 8337EquivEquiv.prodPUnitCITED BYCITES

Cites1

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

  • Equivstatement · cited by 8,337

Cited by9

Results whose statement or proof uses this declaration.