feat(order/antichain): Strong antichains (#11400)

This introduces a predicate `is_strong_antichain` to state that a set is a strong antichain with respect to a relation.

`s` is a strong (upward) antichain wrt `r` if for all `a ≠ b` in `s` there is some `c` such that `¬ r a c` or `¬ r b c`. A strong downward antichain of the swapped relation.

Author: YaelDillies

src/data/set/pairwise.lean

@@ -75,6 +75,9 @@ lemma pairwise.mono (h : t ⊆ s) (hs : s.pairwise r) : t.pairwise r :=
 
 lemma pairwise.mono' (H : r ≤ p) (hr : s.pairwise r) : s.pairwise p := hr.imp H
 
+protected lemma pairwise.eq (hs : s.pairwise r) (ha : a ∈ s) (hb : b ∈ s) (h : ¬ r a b) : a = b :=
+of_not_not $ λ hab, h $ hs ha hb hab
+
 lemma pairwise_top (s : set α) : s.pairwise ⊤ := pairwise_of_forall s _ (λ a b, trivial)
 
 protected lemma subsingleton.pairwise (h : s.subsingleton) (r : α → α → Prop) :
@@ -276,7 +279,7 @@ pairwise_sUnion h
 lemma pairwise_disjoint.elim (hs : s.pairwise_disjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s)
   (h : ¬ disjoint (f i) (f j)) :
   i = j :=
-of_not_not $ λ hij, h $ hs hi hj hij
+hs.eq hi hj h
 
 -- classical
 lemma pairwise_disjoint.elim' (hs : s.pairwise_disjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s)

src/order/antichain.lean

@@ -15,6 +15,8 @@ relation is `G.adj` for `G : simple_graph α`, this corresponds to independent s
 ## Definitions
 
 * `is_antichain r s`: Any two elements of `s : set α` are unrelated by `r : α → α → Prop`.
+* `is_strong_antichain r s`: Any two elements of `s : set α` are not related by `r : α → α → Prop`
+  to a common element.
 * `is_antichain.mk r s`: Turns `s` into an antichain by keeping only the "maximal" elements.
 -/
 
@@ -37,24 +39,24 @@ lemma mono_on (hs : is_antichain r₁ s) (h : s.pairwise (λ ⦃a b⦄, r₂ a b
   is_antichain r₂ s :=
 hs.imp_on $ h.imp $ λ a b h h₁ h₂, h₁ $ h h₂
 
-lemma eq_of_related (hs : is_antichain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : r a b) :
+protected lemma eq (hs : is_antichain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : r a b) :
   a = b :=
-of_not_not $ λ hab, hs ha hb hab h
+hs.eq ha hb $ not_not_intro h
 
-lemma eq_of_related' (hs : is_antichain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : r b a) :
+protected lemma eq' (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
+(hs.eq 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⟩
+⟨λ a b ha _, h.eq trivial trivial ha⟩
 
 protected lemma subsingleton [is_trichotomous α r] (h : is_antichain r s) : s.subsingleton :=
 begin
   rintro a ha b hb,
   obtain hab | hab | hab := trichotomous_of r a b,
-  { exact h.eq_of_related ha hb hab },
+  { exact h.eq ha hb hab },
   { exact hab },
-  { exact (h.eq_of_related hb ha hab).symm }
+  { exact h.eq' ha hb hab }
 end
 
 protected lemma flip (hs : is_antichain r s) : is_antichain (flip r) s :=
@@ -104,11 +106,11 @@ section preorder
 variables [preorder α]
 
 lemma is_antichain_and_least_iff : is_antichain (≤) s ∧ is_least s a ↔ s = {a} :=
-⟨λ h, eq_singleton_iff_unique_mem.2 ⟨h.2.1, λ b hb, h.1.eq_of_related' hb h.2.1 (h.2.2 hb)⟩,
+⟨λ h, eq_singleton_iff_unique_mem.2 ⟨h.2.1, λ b hb, h.1.eq' hb h.2.1 (h.2.2 hb)⟩,
   by { rintro rfl, exact ⟨is_antichain_singleton _ _, is_least_singleton⟩ }⟩
 
 lemma is_antichain_and_greatest_iff : is_antichain (≤) s ∧ is_greatest s a ↔ s = {a} :=
-⟨λ h, eq_singleton_iff_unique_mem.2 ⟨h.2.1, λ b hb, h.1.eq_of_related hb h.2.1 (h.2.2 hb)⟩,
+⟨λ h, eq_singleton_iff_unique_mem.2 ⟨h.2.1, λ b hb, h.1.eq hb h.2.1 (h.2.2 hb)⟩,
   by { rintro rfl, exact ⟨is_antichain_singleton _ _, is_greatest_singleton⟩ }⟩
 
 lemma is_antichain.least_iff (hs : is_antichain (≤) s) : is_least s a ↔ s = {a} :=
@@ -130,3 +132,65 @@ lemma is_antichain.top_mem_iff [order_top α] (hs : is_antichain (≤) s) : ⊤
 is_greatest_top_iff.symm.trans hs.greatest_iff
 
 end preorder
+
+/-! ### Strong antichains -/
+
+/-- An strong (upward) antichain is a set such that no two distinct elements are related to a common
+element. -/
+def is_strong_antichain (r : α → α → Prop) (s : set α) : Prop :=
+s.pairwise $ λ a b, ∀ c, ¬ r a c ∨ ¬ r b c
+
+namespace is_strong_antichain
+
+protected lemma subset (hs : is_strong_antichain r s) (h : t ⊆ s) : is_strong_antichain r t :=
+hs.mono h
+
+lemma mono (hs : is_strong_antichain r₁ s) (h : r₂ ≤ r₁) : is_strong_antichain r₂ s :=
+hs.mono' $ λ a b hab c, (hab c).imp (compl_le_compl h _ _) (compl_le_compl h _ _)
+
+lemma eq (hs : is_strong_antichain r s) {a b c : α} (ha : a ∈ s) (hb : b ∈ s) (hac : r a c)
+  (hbc : r b c) :
+  a = b :=
+hs.eq ha hb $ λ h, false.elim $ (h c).elim (not_not_intro hac) (not_not_intro hbc)
+
+protected lemma is_antichain [is_refl α r] (h : is_strong_antichain r s) : is_antichain r s :=
+h.imp $ λ a b hab, (hab b).resolve_right (not_not_intro $ refl _)
+
+protected lemma subsingleton [is_directed α r] (h : is_strong_antichain r s) : s.subsingleton :=
+λ a ha b hb, let ⟨c, hac, hbc⟩ := directed_of r a b in h.eq ha hb hac hbc
+
+protected lemma flip [is_symm α r] (hs : is_strong_antichain r s) :
+  is_strong_antichain (flip r) s :=
+λ a ha b hb h c, (hs ha hb h c).imp (mt $ symm_of r) (mt $ symm_of r)
+
+lemma swap [is_symm α r] (hs : is_strong_antichain r s) : is_strong_antichain (swap r) s := hs.flip
+
+lemma image (hs : is_strong_antichain r s) {f : α → β} (hf : surjective f)
+  (h : ∀ a b, r' (f a) (f b) → r a b) :
+  is_strong_antichain r' (f '' s) :=
+begin
+  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ hab c,
+  obtain ⟨c, rfl⟩ := hf c,
+  exact (hs ha hb (ne_of_apply_ne _ hab) _).imp (mt $ h _ _) (mt $ h _ _),
+end
+
+lemma preimage (hs : is_strong_antichain r s) {f : β → α} (hf : injective f)
+  (h : ∀ a b, r' a b → r (f a) (f b)) :
+  is_strong_antichain r' (f ⁻¹' s) :=
+λ a ha b hb hab c, (hs ha hb (hf.ne hab) _).imp (mt $ h _ _) (mt $ h _ _)
+
+lemma _root_.is_strong_antichain_insert :
+  is_strong_antichain r (insert a s) ↔ is_strong_antichain r s ∧
+    ∀ ⦃b⦄, b ∈ s → a ≠ b → ∀ c, ¬ r a c ∨ ¬ r b c :=
+set.pairwise_insert_of_symmetric $ λ a b h c, (h c).symm
+
+protected lemma insert (hs : is_strong_antichain r s)
+  (h : ∀ ⦃b⦄, b ∈ s → a ≠ b → ∀ c, ¬ r a c ∨ ¬ r b c) :
+  is_strong_antichain r (insert a s) :=
+is_strong_antichain_insert.2 ⟨hs, h⟩
+
+end is_strong_antichain
+
+lemma set.subsingleton.is_strong_antichain (hs : s.subsingleton) (r : α → α → Prop) :
+  is_strong_antichain r s :=
+hs.pairwise _

src/order/minimal.lean

@@ -84,10 +84,10 @@ lemma inter_maximals_subset : s ∩ maximals r t ⊆ maximals r (s ∩ t) :=
 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⟩
+(maximals_subset _ _).antisymm $ λ a ha, ⟨ha, λ b, h.eq 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⟩
+(minimals_subset _ _).antisymm $ λ a ha, ⟨ha, λ b, h.eq' ha⟩
 
 @[simp] lemma maximals_idem : maximals r (maximals r s) = maximals r s :=
 (maximals_antichain _ _).maximals_eq

src/order/well_founded_set.lean

@@ -214,7 +214,7 @@ begin
   obtain ⟨m, n, hmn, h⟩ := hp (λ n, hi.nat_embedding _ n) (range_subset_iff.2 $
     λ n, (hi.nat_embedding _ n).2),
   exact hmn.ne ((hi.nat_embedding _).injective $ subtype.val_injective $
-    ha.eq_of_related (hi.nat_embedding _ m).2 (hi.nat_embedding _ n).2 h),
+    ha.eq (hi.nat_embedding _ m).2 (hi.nat_embedding _ n).2 h),
 end
 
 lemma finite.partially_well_ordered_on {s : set α} {r : α → α → Prop} [is_refl α r]