add IsBot.isMin_iff

leanprover-community · Nov 20, 2024 · 432124e · 432124e
1 parent 08e5232
commit 432124e
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Mathlib/Order/Max.lean b/Mathlib/Order/Max.lean
@@ -204,6 +204,10 @@ theorem IsTop.isMax_iff {α} [PartialOrder α] {i j : α} (h : IsTop i) : IsMax
   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