feat(Order/Antisymmetrization): comparable minimal elements are equivalent

Author: hawkrobe

Mathlib/Order/Antisymmetrization.lean

@@ -442,6 +442,39 @@ theorem AntisymmRel.symmGen_congr_right (h : AntisymmRel (· ≤ ·) b c) :
 
 end SymmGen
 
+section Minimal
+
+open Relation
+
+variable [Preorder α] {P : α → Prop}
+
+-- TODO: `to_dual` doesn't work with `AntisymmRel` or `SymmGen`.
+theorem Minimal.antisymmRel_of_ge (ha : Minimal P a) (hb : P b) (hge : b ≤ a) :
+    AntisymmRel (· ≤ ·) a b :=
+  ⟨ha.le_of_le hb hge, hge⟩
+
+theorem Maximal.antisymmRel_of_le (ha : Maximal P a) (hb : P b) (hle : a ≤ b) :
+    AntisymmRel (· ≤ ·) a b :=
+  ⟨hle, ha.le_of_ge hb hle⟩
+
+theorem Minimal.antisymmRel_of_symmGen (ha : Minimal P a) (hb : Minimal P b)
+    (hab : SymmGen (· ≤ ·) a b) : AntisymmRel (· ≤ ·) a b :=
+  ⟨hab.elim id (ha.le_of_le hb.prop), hab.elim (hb.le_of_le ha.prop) id⟩
+
+theorem Maximal.antisymmRel_of_symmGen (ha : Maximal P a) (hb : Maximal P b)
+    (hab : SymmGen (· ≤ ·) a b) : AntisymmRel (· ≤ ·) a b :=
+  ⟨hab.elim id (hb.le_of_ge ha.prop), hab.elim (ha.le_of_ge hb.prop) id⟩
+
+end Minimal
+
+theorem Minimal.eq_of_symmGen [PartialOrder α] {P : α → Prop} (ha : Minimal P a)
+    (hb : Minimal P b) (hab : Relation.SymmGen (· ≤ ·) a b) : a = b :=
+  (ha.antisymmRel_of_symmGen hb hab).eq
+
+theorem Maximal.eq_of_symmGen [PartialOrder α] {P : α → Prop} (ha : Maximal P a)
+    (hb : Maximal P b) (hab : Relation.SymmGen (· ≤ ·) a b) : a = b :=
+  (ha.antisymmRel_of_symmGen hb hab).eq
+
 section Prod
 
 variable (α β) [Preorder α] [Preorder β]