Theorems · Definition · category theory
BddLat.dualEquiv
BddLat ≌ BddLat
The equivalence between BddLat and itself induced by OrderDual both ways.
- Defined in
- Mathlib.Order.Category.BddLat
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Equivalencestatement · cited by 601
- CategoryTheory.NatIso.ofComponentsproof · cited by 178
- Lat.carrierproof · cited by 58
- BddLatstatement and proof · cited by 27
- BddLat.toLatproof · cited by 24
- OrderIso.dualDualproof · cited by 8
- BddLat.dualproof · cited by 8
- BddLat.Iso.mkproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- BddLat.dualEquiv_functorstatement and proof · cited by 0
- BddLat.dualEquiv_inversestatement and proof · cited by 0
- latToBddLatCompDualIsoDualCompLatToBddLatproof · cited by 0