diff options
| -rw-r--r-- | mathcomp/ssreflect/order.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index 38ee13d..90ddfcb 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -3549,6 +3549,10 @@ Lemma botEdual : (dual_bottom : L^d) = 1 :> L. Proof. by []. Qed. Lemma topEdual : (dual_top : L^d) = 0 :> L. Proof. by []. Qed. End DualTBLattice. + +Canonical dual_finLatticeType d (T : finLatticeType d) := + [finLatticeType of T^d]. + End DualTBLattice. Module Import TBLatticeTheory. @@ -3682,11 +3686,12 @@ Context {L : tbDistrLatticeType}. Canonical dual_bDistrLatticeType := [bDistrLatticeType of L^d]. Canonical dual_tbDistrLatticeType := [tbDistrLatticeType of L^d]. +End DualTBDistrLattice. + Canonical dual_finDistrLatticeType d (T : finDistrLatticeType d) := [finDistrLatticeType of T^d]. End DualTBDistrLattice. -End DualTBDistrLattice. Module Import TBDistrLatticeTheory. Section TBDistrLatticeTheory. |