Skip to content

Commit bf9761c

Browse files
committed
chore(Order/Defs/PartialOrder): fix naming of DecidableLE' (#31816)
The rename `DecidableGE` -> `DecidableLE'` wasn't done everywhere, and this PR fixes that.
1 parent 8624f6f commit bf9761c

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

Mathlib/Order/Defs/PartialOrder.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -147,7 +147,7 @@ instance instTransGTGE : @Trans α α α GT.gt GE.ge GT.gt := ⟨lt_of_lt_of_le'
147147
instance instTransGEGT : @Trans α α α GE.ge GT.gt GT.gt := ⟨lt_of_le_of_lt'⟩
148148

149149
/-- `<` is decidable if `≤` is. -/
150-
@[to_dual decidableGTOfDecidableGE /-- `<` is decidable if `≤` is. -/]
150+
@[to_dual decidableLT'OfDecidableLE' /-- `<` is decidable if `≤` is. -/]
151151
def decidableLTOfDecidableLE [DecidableLE α] : DecidableLT α :=
152152
fun _ _ => decidable_of_iff _ lt_iff_le_not_ge.symm
153153

@@ -206,7 +206,7 @@ lemma lt_of_le_of_ne : a ≤ b → a ≠ b → a < b := fun h₁ h₂ =>
206206
lt_of_le_not_ge h₁ <| mt (le_antisymm h₁) h₂
207207

208208
/-- Equality is decidable if `≤` is. -/
209-
@[to_dual decidableEqofDecidableGE /-- Equality is decidable if `≤` is. -/]
209+
@[to_dual decidableEqofDecidableLE' /-- Equality is decidable if `≤` is. -/]
210210
def decidableEqOfDecidableLE [DecidableLE α] : DecidableEq α
211211
| a, b =>
212212
if hab : a ≤ b then

0 commit comments

Comments
 (0)