feat(order/minimal): Subset of minimal/maximal elements (#11268)

This defines `minimals r s`/`maximals r s` the minimal/maximal elements of `s` with respect to relation `r`.

src/data/set/basic.lean

@@ -790,6 +790,9 @@ theorem eq_sep_of_subset {s t : set α} (h : s ⊆ t) : s = {x ∈ t | x ∈ s}
 
 @[simp] theorem sep_subset (s : set α) (p : α → Prop) : {x ∈ s | p x} ⊆ s := λ x, and.left
 
+@[simp] lemma sep_empty (p : α → Prop) : {x ∈ (∅ : set α) | p x} = ∅ :=
+by { ext, exact false_and _ }
+
 theorem forall_not_of_sep_empty {s : set α} {p : α → Prop} (H : {x ∈ s | p x} = ∅)
   (x) : x ∈ s → ¬ p x := not_and.1 (eq_empty_iff_forall_not_mem.1 H x : _)
 

src/order/antichain.lean

@@ -41,6 +41,10 @@ lemma eq_of_related (hs : is_antichain r s) {a b : α} (ha : a ∈ s) (hb : b 
   a = b :=
 of_not_not $ λ hab, hs ha hb hab h
 
+lemma eq_of_related' (hs : is_antichain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : r b a) :
+  a = b :=
+(hs.eq_of_related hb ha h).symm
+
 protected lemma is_antisymm (h : is_antichain r univ) : is_antisymm α r :=
 ⟨λ a b ha _, h.eq_of_related trivial trivial ha⟩
 
@@ -88,25 +92,6 @@ lemma insert_of_symmetric (hs : is_antichain r s) (hr : symmetric r)
   is_antichain r (insert a s) :=
 (is_antichain_insert_of_symmetric hr).2 ⟨hs, h⟩
 
-/-- Turns a set into an antichain by keeping only the "maximal" elements. -/
-protected def mk (r : α → α → Prop) (s : set α) : set α := {a ∈ s | ∀ ⦃b⦄, b ∈ s → r a b → a = b}
-
-lemma mk_is_antichain (r : α → α → Prop) (s : set α) : is_antichain r (is_antichain.mk r s) :=
-λ a ha b hb hab h, hab $ ha.2 hb.1 h
-
-lemma mk_subset : is_antichain.mk r s ⊆ s := sep_subset _ _
-
-/-- If `is_antichain.mk r s` is included in but *shadows* the antichain `t`, then it is actually
-equal to `t`. -/
-lemma mk_max (ht : is_antichain r t) (h : is_antichain.mk r s ⊆ t)
-  (hs : ∀ ⦃a⦄, a ∈ t → ∃ b ∈ is_antichain.mk r s, r a b) :
-  t = is_antichain.mk r s :=
-begin
-  refine subset.antisymm (λ a ha, _) h,
-  obtain ⟨b, hb, hr⟩ := hs ha,
-  rwa of_not_not (λ hab, ht ha (h hb) hab hr),
-end
-
 end is_antichain
 
 lemma set.subsingleton.is_antichain (hs : s.subsingleton) (r : α → α → Prop): is_antichain r s :=

src/order/basic.lean

@@ -48,10 +48,6 @@ provide many aliases to dot notation-less lemmas. For example, `le_trans` is ali
 - expand module docs
 - automatic construction of dual definitions / theorems
 
-## See also
-
-- `algebra.order.basic` for basic lemmas about orders, and projection notation for orders
-
 ## Tags
 
 preorder, order, partial order, poset, linear order, chain
@@ -62,12 +58,16 @@ open function
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w} {r : α → α → Prop}
 
+lemma ge_antisymm [partial_order α] {a b : α} (hab : a ≤ b) (hba : b ≤ a) : b = a :=
+le_antisymm hba hab
+
 attribute [simp] le_refl
 attribute [ext] has_le
 
 alias le_trans        ← has_le.le.trans
 alias lt_of_le_of_lt  ← has_le.le.trans_lt
 alias le_antisymm     ← has_le.le.antisymm
+alias ge_antisymm     ← has_le.le.antisymm'
 alias lt_of_le_of_ne  ← has_le.le.lt_of_ne
 alias lt_of_le_not_le ← has_le.le.lt_of_not_le
 alias lt_or_eq_of_le  ← has_le.le.lt_or_eq

src/order/minimal.lean

@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import order.antichain
+
+/-!
+# Minimal/maximal elements of a set
+
+This file defines minimal and maximal of a set with respect to an arbitrary relation.
+
+## Main declarations
+
+* `maximals r s`: Maximal elements of `s` with respect to `r`.
+* `minimals r s`: Minimal elements of `s` with respect to `r`.
+
+## TODO
+
+Do we need a `finset` version?
+-/
+
+open function set
+
+variables {α : Type*} (r r₁ r₂ : α → α → Prop) (s t : set α) (a : α)
+
+/-- Turns a set into an antichain by keeping only the "maximal" elements. -/
+def maximals : set α := {a ∈ s | ∀ ⦃b⦄, b ∈ s → r a b → a = b}
+
+/-- Turns a set into an antichain by keeping only the "maximal" elements. -/
+def minimals : set α := {a ∈ s | ∀ ⦃b⦄, b ∈ s → r b a → a = b}
+
+lemma maximals_subset : maximals r s ⊆ s := sep_subset _ _
+lemma minimals_subset : minimals r s ⊆ s := sep_subset _ _
+
+@[simp] lemma maximals_empty : maximals r ∅ = ∅ := sep_empty _
+@[simp] lemma minimals_empty : minimals r ∅ = ∅ := sep_empty _
+
+@[simp] lemma maximals_singleton : maximals r {a} = {a} :=
+(maximals_subset _ _).antisymm $ singleton_subset_iff.2 $ ⟨rfl, λ b hb _, hb.symm⟩
+
+@[simp] lemma minimals_singleton : minimals r {a} = {a} := maximals_singleton _ _
+
+lemma maximals_swap : maximals (swap r) s = minimals r s := rfl
+lemma minimals_swap : minimals (swap r) s = maximals r s := rfl
+
+lemma maximals_antichain : is_antichain r (maximals r s) := λ a ha b hb hab h, hab $ ha.2 hb.1 h
+lemma minimals_antichain : is_antichain r (minimals r s) := (maximals_antichain _ _).swap
+
+lemma maximals_eq_minimals [is_symm α r] : maximals r s = minimals r s :=
+by { congr, ext a b, exact comm }
+
+variables {r r₁ r₂ s t a}
+
+lemma set.subsingleton.maximals_eq (h : s.subsingleton) : maximals r s = s :=
+h.induction_on (minimals_empty _) (maximals_singleton _)
+
+lemma set.subsingleton.minimals_eq (h : s.subsingleton) : minimals r s = s := h.maximals_eq
+
+lemma maximals_mono (h : ∀ a b, r₁ a b → r₂ a b) : maximals r₂ s ⊆ maximals r₁ s :=
+λ a ha, ⟨ha.1, λ b hb, ha.2 hb ∘ h _ _⟩
+
+lemma minimals_mono (h : ∀ a b, r₁ a b → r₂ a b) : minimals r₂ s ⊆ minimals r₁ s :=
+λ a ha, ⟨ha.1, λ b hb, ha.2 hb ∘ h _ _⟩
+
+lemma maximals_union : maximals r (s ∪ t) ⊆ maximals r s ∪ maximals r t :=
+begin
+  intros a ha,
+  obtain h | h := ha.1,
+  { exact or.inl ⟨h, λ b hb, ha.2 $ or.inl hb⟩ },
+  { exact or.inr ⟨h, λ b hb, ha.2 $ or.inr hb⟩ }
+end
+
+lemma minimals_union : minimals r (s ∪ t) ⊆ minimals r s ∪ minimals r t := maximals_union
+
+lemma maximals_inter_subset : maximals r s ∩ t ⊆ maximals r (s ∩ t) :=
+λ a ha, ⟨⟨ha.1.1, ha.2⟩, λ b hb, ha.1.2 hb.1⟩
+
+lemma minimals_inter_subset : minimals r s ∩ t ⊆ minimals r (s ∩ t) := maximals_inter_subset
+
+lemma inter_maximals_subset : s ∩ maximals r t ⊆ maximals r (s ∩ t) :=
+λ a ha, ⟨⟨ha.1, ha.2.1⟩, λ b hb, ha.2.2 hb.2⟩
+
+lemma inter_minimals_subset : s ∩ minimals r t ⊆ minimals r (s ∩ t) := inter_maximals_subset
+
+lemma _root_.is_antichain.maximals_eq (h : is_antichain r s) : maximals r s = s :=
+(maximals_subset _ _).antisymm $ λ a ha, ⟨ha, λ b, h.eq_of_related ha⟩
+
+lemma _root_.is_antichain.minimals_eq (h : is_antichain r s) : minimals r s = s :=
+(minimals_subset _ _).antisymm $ λ a ha, ⟨ha, λ b, h.eq_of_related' ha⟩
+
+@[simp] lemma maximals_idem : maximals r (maximals r s) = maximals r s :=
+(maximals_antichain _ _).maximals_eq
+
+@[simp] lemma minimals_idem : minimals r (minimals r s) = minimals r s := maximals_idem
+
+/-- If `maximals r s` is included in but *shadows* the antichain `t`, then it is actually
+equal to `t`. -/
+lemma is_antichain.max_maximals (ht : is_antichain r t) (h : maximals r s ⊆ t)
+  (hs : ∀ ⦃a⦄, a ∈ t → ∃ b ∈ maximals r s, r b a) :
+  maximals r s = t :=
+begin
+  refine h.antisymm (λ a ha, _),
+  obtain ⟨b, hb, hr⟩ := hs ha,
+  rwa of_not_not (λ hab, ht (h hb) ha (ne.symm hab) hr),
+end
+
+/-- If `minimals r s` is included in but *shadows* the antichain `t`, then it is actually
+equal to `t`. -/
+lemma is_antichain.max_minimals (ht : is_antichain r t) (h : minimals r s ⊆ t)
+  (hs : ∀ ⦃a⦄, a ∈ t → ∃ b ∈ minimals r s, r a b) :
+  minimals r s = t :=
+begin
+  refine h.antisymm (λ a ha, _),
+  obtain ⟨b, hb, hr⟩ := hs ha,
+  rwa of_not_not (λ hab, ht ha (h hb) hab hr),
+end
+
+variables [partial_order α]
+
+lemma is_least.mem_minimals (h : is_least s a) : a ∈ minimals (≤) s :=
+⟨h.1, λ b hb, (h.2 hb).antisymm⟩
+
+lemma is_greatest.mem_maximals (h : is_greatest s a) : a ∈ maximals (≤) s :=
+⟨h.1, λ b hb, (h.2 hb).antisymm'⟩
+
+lemma is_least.minimals_eq (h : is_least s a) : minimals (≤) s = {a} :=
+eq_singleton_iff_unique_mem.2 ⟨h.mem_minimals, λ b hb, hb.2 h.1 $ h.2 hb.1⟩
+
+lemma is_greatest.maximals_eq (h : is_greatest s a) : maximals (≤) s = {a} :=
+eq_singleton_iff_unique_mem.2 ⟨h.mem_maximals, λ b hb, hb.2 h.1 $ h.2 hb.1⟩

src/order/rel_classes.lean

@@ -26,6 +26,13 @@ This lemma matches the lemmas from lean core in `init.algebra.classes`, but is m
 @[elab_simple]
 lemma antisymm_of (r : α → α → Prop) [is_antisymm α r] {a b : α} : r a b → r b a → a = b := antisymm
 
+lemma comm [is_symm α r] {a b : α} : r a b ↔ r b a := ⟨symm, symm⟩
+
+/-- A version of `comm` with `r` explicit.
+
+This lemma matches the lemmas from lean core in `init.algebra.classes`, but is missing there.  -/
+lemma comm_of (r : α → α → Prop) [is_symm α r] {a b : α} : r a b ↔ r b a := comm
+
 theorem is_refl.swap (r) [is_refl α r] : is_refl α (swap r) := ⟨refl_of r⟩
 theorem is_irrefl.swap (r) [is_irrefl α r] : is_irrefl α (swap r) := ⟨irrefl_of r⟩
 theorem is_trans.swap (r) [is_trans α r] : is_trans α (swap r) :=