Mathlib Map

Theorems · Definition · order theory

OrderIso.dualDual

(α : Type u_2) → [inst : LE α] → α ≃o αᵒᵈᵒᵈ

The order isomorphism between a type and its double dual.

Defined in
Mathlib.Order.Hom.Basic
Cited by
8 results in Mathlib
Foundations
Depth 17 from the axioms · uses Quot.sound
Assumes
LE
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar · cited by 4Rat.intermediateFieldEqui…FinPartOrd.dualEquiv · cited by 4FinPartOrd.dualEquivBddDistLat.dualEquiv · cited by 2BddDistLat.dualEquivNonemptyFinLinOrd.dualEquiv · cited by 2NonemptyFinLinOrd.dualEqu…FinBoolAlg.dualEquiv · cited by 2FinBoolAlg.dualEquivPreord.dualEquiv · cited by 2Preord.dualEquivBoolAlg.dualEquiv · cited by 2BoolAlg.dualEquivLinOrd.dualEquiv · cited by 2LinOrd.dualEquivSemilatSupCatEquivSemilatInfCat · cited by 2SemilatSupCatEquivSemilat…PartOrdEmb.dualEquiv · cited by 2PartOrdEmb.dualEquivBddOrd.dualEquiv · cited by 2BddOrd.dualEquivFinBddDistLat.dualEquiv · cited by 2FinBddDistLat.dualEquivPartOrd.dualEquiv · cited by 2PartOrd.dualEquivDistLat.dualEquiv · cited by 2DistLat.dualEquivCompleteLat.dualEquiv · cited by 2CompleteLat.dualEquivOrderDual · cited by 927OrderDualOrderIso · cited by 874OrderIsoOrderIso.refl · cited by 24OrderIso.reflOrderIso.dualDualCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by25

Results whose statement or proof uses this declaration.