feat(Order/Max): add IsTop.isMax_iff and IsBot.isMin_iff (#19305)

Upstreamed from the [Carleson](https://github.com/fpvandoorn/carleson) project. 

Co-authored-by: Floris van Doorn

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