Skip to content

Commit b0dc93c

Browse files
YaelDilliestannerduve
authored andcommitted
chore(Order/WithBot): fix recent deprecations (#23761)
1 parent 2340a70 commit b0dc93c

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

Mathlib/Order/WithBot.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -819,8 +819,8 @@ lemma eq_top_iff_forall_gt : y = ⊤ ↔ ∀ a : α, a < y := by
819819
lemma eq_top_iff_forall_ge [NoMaxOrder α] : y = ⊤ ↔ ∀ a : α, a ≤ y :=
820820
WithBot.eq_bot_iff_forall_le (α := αᵒᵈ)
821821

822-
@[deprecated (since := "2025-03-19")] alias forall_lt_iff_eq_top := eq_top_iff_forall_gt
823-
@[deprecated (since := "2025-03-19")] alias forall_le_iff_eq_top := eq_top_iff_forall_ge
822+
@[deprecated (since := "2025-03-19")] alias forall_gt_iff_eq_top := eq_top_iff_forall_gt
823+
@[deprecated (since := "2025-03-19")] alias forall_ge_iff_eq_top := eq_top_iff_forall_ge
824824

825825
lemma forall_coe_le_iff_le [NoMaxOrder α] {x y : WithTop α} : (∀ a : α, a ≤ x → a ≤ y) ↔ x ≤ y := by
826826
obtain _ | x := x

0 commit comments

Comments
 (0)