Theorems · Theorem · order theory
FinBoolAlg.dual_map
∀ {X Y : FinBoolAlg} (f : X ⟶ Y),
FinBoolAlg.dual.map f =
CategoryTheory.InducedCategory.homMk (BoolAlg.ofHom (BoundedLatticeHom.dual (BoolAlg.Hom.hom f.hom)))- Defined in
- Mathlib.Order.Category.FinBoolAlg
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Functor.mapstatement and proof · cited by 8,698
- Equivstatement · cited by 8,337
- OrderDualstatement · cited by 927
- CategoryTheory.InducedCategory.Hom.homstatement · cited by 850
- BoundedLatticeHomstatement · cited by 185
- CategoryTheory.InducedCategorystatement · cited by 71
- BoolAlgstatement · cited by 47
- BoolAlg.carrierstatement · cited by 44
- CategoryTheory.InducedCategory.homMkstatement · cited by 33
- FinBoolAlgstatement and proof · cited by 15
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.