feat(order/antichain): Antichains are order-connected (#18636)

src/data/set/intervals/ord_connected.lean

@@ -5,6 +5,7 @@ Authors: Yury G. Kudryashov
 -/
 import data.set.intervals.unordered_interval
 import data.set.lattice
+import order.antichain
 
 /-!
 # Order-connected sets
@@ -173,6 +174,15 @@ dual_ord_connected_iff.2 ‹_›
 
 end preorder
 
+section partial_order
+variables {α : Type*} [partial_order α] {s : set α}
+
+protected lemma is_antichain.ord_connected (hs : is_antichain (≤) s) : s.ord_connected :=
+⟨λ x hx y hy z hz, by { obtain rfl := hs.eq hx hy (hz.1.trans hz.2),
+  rw [Icc_self, mem_singleton_iff] at hz, rwa hz }⟩
+
+end partial_order
+
 section linear_order
 variables {α : Type*} [linear_order α] {s : set α} {x : α}
 

src/order/antichain.lean

@@ -26,7 +26,7 @@ relation is `G.adj` for `G : simple_graph α`, this corresponds to independent s
 open function set
 
 section general
-variables {α β : Type*} {r r₁ r₂ : α → α → Prop} {r' : β → β → Prop} {s t : set α} {a : α}
+variables {α β : Type*} {r r₁ r₂ : α → α → Prop} {r' : β → β → Prop} {s t : set α} {a b : α}
 
 protected lemma symmetric.compl (h : symmetric r) : symmetric rᶜ := λ x y hr hr', hr $ h hr'
 
@@ -176,6 +176,9 @@ hs.pairwise _
 section preorder
 variables [preorder α]
 
+lemma is_antichain.not_lt (hs : is_antichain (≤) s) (ha : a ∈ s) (hb : b ∈ s) : ¬ a < b :=
+λ h, hs ha hb h.ne h.le
+
 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' hb h.2.1 (h.2.2 hb)⟩,
   by { rintro rfl, exact ⟨is_antichain_singleton _ _, is_least_singleton⟩ }⟩
@@ -204,6 +207,14 @@ is_greatest_top_iff.symm.trans hs.greatest_iff
 
 end preorder
 
+section partial_order
+variables [partial_order α]
+
+lemma is_antichain_iff_forall_not_lt : is_antichain (≤) s ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → ¬ a < b :=
+⟨λ hs a ha b, hs.not_lt ha, λ hs a ha b hb h h', hs ha hb $ h'.lt_of_ne h⟩
+
+end partial_order
+
 /-! ### Strong antichains -/
 
 /-- A strong (upward) antichain is a set such that no two distinct elements are related to a common