Skip to content

Commit 006b9a9

Browse files
committed
Update Basic.lean
1 parent efc0e39 commit 006b9a9

1 file changed

Lines changed: 2 additions & 0 deletions

File tree

Mathlib/Order/BoundedOrder/Basic.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -263,6 +263,8 @@ class BoundedOrder (α : Type u) [LE α] extends OrderTop α, OrderBot α
263263
attribute [to_dual self (reorder := 3 4)] BoundedOrder.mk
264264
attribute [to_dual existing] BoundedOrder.toOrderTop
265265

266+
instance {α : Type*} [LE α] [OrderTop α] [OrderBot α] : BoundedOrder α where
267+
266268
instance OrderDual.instBoundedOrder (α : Type u) [LE α] [BoundedOrder α] : BoundedOrder αᵒᵈ where
267269
__ := inferInstanceAs (OrderTop αᵒᵈ)
268270
__ := inferInstanceAs (OrderBot αᵒᵈ)

0 commit comments

Comments
 (0)