Theorems · Definition · order theory
FinBoolAlg.dualEquiv
FinBoolAlg ≌ FinBoolAlg
The equivalence between FinBoolAlg and itself induced by OrderDual both ways.
- Defined in
- Mathlib.Order.Category.FinBoolAlg
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 68 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
- BoolAlg.carrierproof · cited by 44
- FinBoolAlgstatement and proof · cited by 15
- FinBoolAlg.toBoolAlgproof · cited by 10
- OrderIso.dualDualproof · cited by 8
- FinBoolAlg.dualproof · cited by 4
- FinBoolAlg.Iso.mkproof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- FinBoolAlg.dualEquiv_functorstatement and proof · cited by 0
- FinBoolAlg.dualEquiv_inversestatement and proof · cited by 0