Skip to content

Commit d9165c9

Browse files
committed
fix
1 parent 7590793 commit d9165c9

1 file changed

Lines changed: 0 additions & 1 deletion

File tree

  • Mathlib/Order/ConditionallyCompleteLattice

Mathlib/Order/ConditionallyCompleteLattice/Defs.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,6 @@ class ConditionallyCompleteLinearOrder (α : Type*)
8282
compareOfLessAndEq_rfl
8383

8484
attribute [to_dual existing] ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove
85-
attribute [to_dual existing] ConditionallyCompleteLinearOrder.csInf_of_not_bddBelow
8685

8786
/-- A conditionally complete linear order with `Bot` is a linear order with least element, in which
8887
every nonempty subset which is bounded above has a supremum, and every nonempty subset (necessarily

0 commit comments

Comments
 (0)