Theorems · Definition · order theory
OrderDual.ofDual
{α : Type u_1} → αᵒᵈ ≃ αofDual is the identity function from the OrderDual of a linear order.
- Defined in
- Mathlib.Order.OrderDual
- Cited by
- 400 results in Mathlib
- Foundations
- Depth 11 from the axioms, rests on 40 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement · cited by 8,337
- OrderDualstatement and proof · cited by 927
- Equiv.reflproof · cited by 274
Cited by443
Results whose statement or proof uses this declaration.
- OrderHom.dualproof · cited by 48
- Monotone.dualstatement · cited by 39
- Antitone.dual_leftstatement · cited by 33
- CategoryTheory.orderDualEquivalenceproof · cited by 15
- Ideal.exists_minimalPrimes_leproof · cited by 14
- Set.Icc_toDualstatement · cited by 13
- Submodule.dualAnnihilator_gcstatement · cited by 13
- Fin.revOrderIsoproof · cited by 11
- Set.Ico_toDualstatement · cited by 11
- eVariationOn.comp_ofDualstatement and proof · cited by 11
- BoundedVariationOn.ofDualstatement · cited by 11
- Set.Ioo_toDualstatement · cited by 11
Showing the 200 most cited of 443.