diff --git a/Mathlib/Order/WithBot.lean b/Mathlib/Order/WithBot.lean index e87a5e9ddf00f3..dcb03338b18063 100644 --- a/Mathlib/Order/WithBot.lean +++ b/Mathlib/Order/WithBot.lean @@ -819,8 +819,8 @@ lemma eq_top_iff_forall_gt : y = ⊤ ↔ ∀ a : α, a < y := by lemma eq_top_iff_forall_ge [NoMaxOrder α] : y = ⊤ ↔ ∀ a : α, a ≤ y := WithBot.eq_bot_iff_forall_le (α := αᵒᵈ) -@[deprecated (since := "2025-03-19")] alias forall_lt_iff_eq_top := eq_top_iff_forall_gt -@[deprecated (since := "2025-03-19")] alias forall_le_iff_eq_top := eq_top_iff_forall_ge +@[deprecated (since := "2025-03-19")] alias forall_gt_iff_eq_top := eq_top_iff_forall_gt +@[deprecated (since := "2025-03-19")] alias forall_ge_iff_eq_top := eq_top_iff_forall_ge lemma forall_coe_le_iff_le [NoMaxOrder α] {x y : WithTop α} : (∀ a : α, a ≤ x → a ≤ y) ↔ x ≤ y := by obtain _ | x := x