diff --git a/Mathlib/Order/Max.lean b/Mathlib/Order/Max.lean
index 36518a3cb4aa5..7cf8fc7da8e5c 100644
--- a/Mathlib/Order/Max.lean
+++ b/Mathlib/Order/Max.lean
@@ -200,6 +200,14 @@ protected theorem IsBot.isMin (h : IsBot a) : IsMin a := fun b _ => h b
 
 protected theorem IsTop.isMax (h : IsTop a) : IsMax a := fun b _ => h b
 
+theorem IsTop.isMax_iff {α} [PartialOrder α] {i j : α} (h : IsTop i) : IsMax j ↔ j = i := by
+  simp_rw [le_antisymm_iff, h j, true_and]
+  exact ⟨(· (h j)), Function.swap (fun _ ↦ h · |>.trans ·)⟩
+
+theorem IsBot.isMin_iff {α} [PartialOrder α] {i j : α} (h : IsBot i) : IsMin j ↔ j = i := by
+  simp_rw [le_antisymm_iff, h j, and_true]
+  exact ⟨fun a ↦ a (h j), fun a h' ↦ fun _ ↦ Preorder.le_trans j i h' a (h h')⟩
+
 @[simp]
 theorem isBot_toDual_iff : IsBot (toDual a) ↔ IsTop a :=
   Iff.rfl