feat(order/well_founded_set): defining is_partially_well_ordered to…

… prove `is_wf.add` (#6226)

Defines `set.is_partially_well_ordered s`, equivalent to any infinite sequence to `s` contains an infinite monotone subsequence
Provides a basic API for `set.is_partially_well_ordered`
Proves `is_wf.add` and `is_wf.mul`

src/order/well_founded_set.lean

@@ -7,6 +7,7 @@ import data.set.finite
 import data.fintype.basic
 import order.well_founded
 import order.order_iso_nat
+import algebra.pointwise
 
 /-!
 # Well-founded sets
@@ -17,6 +18,8 @@ A well-founded subset of an ordered type is one on which the relation `<` is wel
  * `set.well_founded_on s r` indicates that the relation `r` is
   well-founded when restricted to the set `s`.
  * `set.is_wf s` indicates that `<` is well-founded when restricted to `s`.
+ * `set.is_partially_well_ordered s` indicates that any infinite sequence of elements in `s`
+  contains an infinite monotone subsequence.
 
 ### Definitions for Hahn Series
  * `set.add_antidiagonal s t a` and `set.mul_antidiagonal s t a` are the sets of pairs of elements
@@ -144,13 +147,6 @@ fintype.preorder.well_founded
 namespace set
 variables [partial_order α] {s : set α} {a : α}
 
-@[simp]
-theorem is_wf_singleton : is_wf ({a} : set α) :=
-by simp [← finset.coe_singleton]
-
-theorem is_wf.insert (hs : is_wf s) : is_wf (insert a s) :=
-by { rw ← union_singleton, exact hs.union is_wf_singleton }
-
 theorem finite.is_wf (h : s.finite) : s.is_wf :=
 begin
   rw ← h.coe_to_finset,
@@ -160,6 +156,137 @@ end
 @[simp]
 theorem fintype.is_wf [fintype α] : s.is_wf := (finite.of_fintype s).is_wf
 
+@[simp]
+theorem is_wf_empty : is_wf (∅ : set α) :=
+finite_empty.is_wf
+
+@[simp]
+theorem is_wf_singleton (a) : is_wf ({a} : set α) :=
+(finite_singleton a).is_wf
+
+theorem is_wf.insert (a) (hs : is_wf s) : is_wf (insert a s) :=
+by { rw ← union_singleton, exact hs.union (is_wf_singleton a) }
+
+end set
+
+namespace set
+
+/-- A subset of a preorder is partially well-ordered when any infinite sequence contains
+  a monotone subsequence of length 2 (or equivalently, an infinite monotone subsequence). -/
+def is_partially_well_ordered [preorder α] (s) : Prop :=
+  ∀ (f : ℕ → α), range f ⊆ s → ∃ (m n : ℕ), m < n ∧ f m ≤ f n
+
+section partial_order
+variables [partial_order α] {s : set α} {t : set α}
+
+lemma is_partially_well_ordered.is_wf (h : s.is_partially_well_ordered) :
+  s.is_wf :=
+begin
+  rw is_wf_iff_no_descending_seq,
+  intros f con,
+  obtain ⟨m, n, hlt, hle⟩ := h f con,
+  exact not_lt_of_le hle (f.lt_iff_lt.2 hlt),
+end
+
+theorem is_partially_well_ordered.exists_monotone_subseq
+  (h : s.is_partially_well_ordered) (f : ℕ → α) (hf : range f ⊆ s) :
+  ∃ (g : ℕ ↪o ℕ), monotone (f ∘ g) :=
+begin
+  obtain ⟨g, h1 | h2⟩ := exists_increasing_or_nonincreasing_subseq (≤) f,
+  { refine ⟨g, λ m n hle, _⟩,
+    obtain hlt | heq := lt_or_eq_of_le hle,
+    { exact h1 m n hlt, },
+    { rw [heq] } },
+  { exfalso,
+    obtain ⟨m, n, hlt, hle⟩ := h (f ∘ g) (subset.trans (range_comp_subset_range _ _) hf),
+    exact h2 m n hlt hle }
+end
+
+theorem is_partially_well_ordered_iff_exists_monotone_subseq :
+  s.is_partially_well_ordered ↔
+    ∀ f : ℕ → α, range f ⊆ s → ∃ (g : ℕ ↪o ℕ), monotone (f ∘ g) :=
+begin
+  classical,
+  split; intros h f hf,
+  { exact h.exists_monotone_subseq f hf },
+  { obtain ⟨g, gmon⟩ := h f hf,
+    refine ⟨g 0, g 1, g.lt_iff_lt.2 zero_lt_one, gmon zero_le_one⟩, }
+end
+
+lemma is_partially_well_ordered.prod (hs : s.is_partially_well_ordered)
+  (ht : t.is_partially_well_ordered) :
+  (s.prod t).is_partially_well_ordered :=
+begin
+  classical,
+  rw is_partially_well_ordered_iff_exists_monotone_subseq at *,
+  intros f hf,
+  obtain ⟨g1, h1⟩ := hs (prod.fst ∘ f) _,
+  swap,
+  { rw [range_comp, image_subset_iff],
+    refine subset.trans hf _,
+    rintros ⟨x1, x2⟩ hx,
+    simp only [mem_preimage, hx.1] },
+  obtain ⟨g2, h2⟩ := ht (prod.snd ∘ f ∘ g1) _,
+  refine ⟨g2.trans g1, λ m n mn, _⟩,
+  swap,
+  { rw [range_comp, image_subset_iff],
+    refine subset.trans (range_comp_subset_range _ _) (subset.trans hf _),
+    rintros ⟨x1, x2⟩ hx,
+    simp only [mem_preimage, hx.2] },
+  simp only [rel_embedding.coe_trans, function.comp_app],
+  exact ⟨h1 (g2.le_iff_le.2 mn), h2 mn⟩,
+end
+
+theorem is_partially_well_ordered.image_of_monotone {β : Type*} [partial_order β]
+  (hs : s.is_partially_well_ordered) {f : α → β} (hf : monotone f) :
+  is_partially_well_ordered (f '' s) :=
+λ g hg, begin
+  have h := λ (n : ℕ), ((mem_image _ _ _).1 (hg (mem_range_self n))),
+  obtain ⟨m, n, hlt, hmn⟩ := hs (λ n, classical.some (h n)) _,
+  { refine ⟨m, n, hlt, _⟩,
+    rw [← (classical.some_spec (h m)).2,
+      ← (classical.some_spec (h n)).2],
+    apply hf hmn },
+  { rintros _ ⟨n, rfl⟩,
+    exact (classical.some_spec (h n)).1 }
+end
+
+end partial_order
+
+theorem is_wf.is_partially_well_ordered [linear_order α] {s : set α}
+  (hs : s.is_wf) : s.is_partially_well_ordered :=
+λ f hf, begin
+  rw [is_wf, well_founded_on_iff] at hs,
+  have hrange : (range f).nonempty := ⟨f 0, mem_range_self 0⟩,
+  let a := hs.min (range f) hrange,
+  obtain ⟨m, hm⟩ := hs.min_mem (range f) hrange,
+  refine ⟨m, m.succ, m.lt_succ_self, le_of_not_lt (λ con, _)⟩,
+  rw hm at con,
+  apply hs.not_lt_min (range f) hrange (mem_range_self m.succ)
+    ⟨con, hf (mem_range_self m.succ), hf _⟩,
+  rw ← hm,
+  apply mem_range_self,
+end
+
+section
+
+variables [linear_ordered_cancel_comm_monoid α] {s : set α} {t : set α}
+
+@[to_additive]
+theorem is_partially_well_ordered.mul
+  (hs : s.is_partially_well_ordered) (ht : t.is_partially_well_ordered) :
+  is_partially_well_ordered (s * t) :=
+begin
+  rw ← image_mul_prod,
+  exact (is_partially_well_ordered.prod hs ht).image_of_monotone (λ _ _ h, mul_le_mul' h.1 h.2),
+end
+
+@[to_additive]
+theorem is_wf.mul (hs : s.is_wf) (ht : t.is_wf) : is_wf (s * t) :=
+(hs.is_partially_well_ordered.mul ht.is_partially_well_ordered).is_wf
+
+end
+
 end set
 
 theorem not_well_founded_swap_of_infinite_of_well_order
@@ -185,8 +312,8 @@ namespace set
 
 /-- `set.mul_antidiagonal s t a` is the set of all pairs of an element in `s` and an element in `t`
   that multiply to `a`. -/
-@[to_additive "`set.add_antidiagonal s t a` is the set of all pairs of an element in `s` and an
-  element in `t` that add to `a`."]
+@[to_additive "`set.add_antidiagonal s t a` is the set of all pairs of an element in `s`
+  and an element in `t` that add to `a`."]
 def mul_antidiagonal [monoid α] (s t : set α) (a : α) : set (α × α) :=
 { x | x.1 * x.2 = a ∧ x.1 ∈ s ∧ x.2 ∈ t }
 
@@ -289,11 +416,40 @@ variables {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (a : α)
 noncomputable def mul_antidiagonal : finset (α × α) :=
 (set.mul_antidiagonal.finite_of_is_wf hs ht a).to_finset
 
-variables {hs} {ht} {a} {x : α × α}
+variables {hs} {ht} {u : set α} {hu : u.is_wf} {a} {x : α × α}
 
 @[simp, to_additive]
 lemma mem_mul_antidiagonal :
   x ∈ mul_antidiagonal hs ht a ↔ x.1 * x.2 = a ∧ x.1 ∈ s ∧ x.2 ∈ t :=
 by simp [mul_antidiagonal]
 
+@[to_additive]
+lemma mul_antidiagonal_mono_left (hus : u ⊆ s) :
+  (finset.mul_antidiagonal hu ht a) ⊆ (finset.mul_antidiagonal hs ht a) :=
+λ x hx, begin
+  rw mem_mul_antidiagonal at *,
+  exact ⟨hx.1, hus hx.2.1, hx.2.2⟩,
+end
+
+@[to_additive]
+lemma mul_antidiagonal_mono_right (hut : u ⊆ t) :
+  (finset.mul_antidiagonal hs hu a) ⊆ (finset.mul_antidiagonal hs ht a) :=
+λ x hx, begin
+  rw mem_mul_antidiagonal at *,
+  exact ⟨hx.1, hx.2.1, hut hx.2.2⟩,
+end
+
+@[to_additive]
+lemma support_mul_antidiagonal_subset_mul :
+  { a : α | (mul_antidiagonal hs ht a).nonempty } ⊆ s * t :=
+(λ x ⟨⟨a1, a2⟩, ha⟩, begin
+  obtain ⟨hmul, h1, h2⟩ := mem_mul_antidiagonal.1 ha,
+  exact ⟨a1, a2, h1, h2, hmul⟩,
+end)
+
+@[to_additive]
+theorem is_wf_support_mul_antidiagonal :
+  { a : α | (mul_antidiagonal hs ht a).nonempty }.is_wf :=
+(hs.mul ht).mono support_mul_antidiagonal_subset_mul
+
 end finset