Theorems · Definition · order theory
OrderIso.equivalence
{X : Type u} → {Y : Type v} → [inst : Preorder X] → [inst_1 : Preorder Y] → X ≃o Y → (X ≌ Y)The equivalence of categories X ≌ Y induced by e : X ≃o Y.
- Defined in
- Mathlib.CategoryTheory.Category.Preorder
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 29 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- OrderIsostatement and proof · cited by 874
- CategoryTheory.Equivalencestatement · cited by 601
- CategoryTheory.NatIso.ofComponentsproof · cited by 178
- CategoryTheory.eqToIsoproof · cited by 97
- Monotone.functorproof · cited by 66
- OrderIso.monotoneproof · cited by 23
Cited by20
Results whose statement or proof uses this declaration.
- TopologicalSpace.Opens.mapMapIsoproof · cited by 12
- CategoryTheory.ComposableArrows.opEquivalenceproof · cited by 10
- CategoryTheory.TransfiniteCompositionOfShape.ofOrderIsoproof · cited by 3
- CategoryTheory.Limits.hasColimitsOfShape_of_initialSegproof · cited by 1
- CategoryTheory.Limits.hasColimitsOfShape_of_isSuccLimit'proof · cited by 1
- CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_appstatement and proof · cited by 0
- CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_appstatement and proof · cited by 0
- CategoryTheory.ComposableArrows.opEquivalence_functor_map_appstatement · cited by 0
- CategoryTheory.ComposableArrows.opEquivalence_functor_obj_mapstatement · cited by 0
- CategoryTheory.ComposableArrows.opEquivalence_inverse_mapstatement · cited by 0
- CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_appstatement and proof · cited by 0
- CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_appstatement and proof · cited by 0