feat(order/order_iso_nat): add another flavour of well-foundedness fo…

…r partial orders (#5434)

src/order/order_iso_nat.lean

@@ -7,6 +7,7 @@ import data.nat.basic
 import data.equiv.denumerable
 import data.set.finite
 import order.rel_iso
+import order.preorder_hom
 import logic.function.iterate
 
 namespace rel_embedding
@@ -141,3 +142,18 @@ begin
       exact ih (lt_of_lt_of_le m.lt_succ_self (nat.le_add_right _ _)) } },
   { exact ⟨g, or.intro_right _ hnr⟩ }
 end
+
+/-- The "monotone chain condition" below is sometimes a convenient form of well foundedness. -/
+lemma well_founded.monotone_chain_condition (α : Type*) [partial_order α] :
+  well_founded ((>) : α → α → Prop) ↔ ∀ (a : ℕ →ₘ α), ∃ n, ∀ m, n ≤ m → a n = a m :=
+begin
+  split; intros h,
+  { rw well_founded.well_founded_iff_has_max' at h,
+    intros a, have hne : (set.range a).nonempty, { use a 0, simp, },
+    obtain ⟨x, ⟨n, hn⟩, range_bounded⟩ := h _ hne,
+    use n, intros m hm, rw ← hn at range_bounded, symmetry,
+    apply range_bounded (a m) (set.mem_range_self _) (a.monotone hm), },
+  { rw rel_embedding.well_founded_iff_no_descending_seq, rintros ⟨a⟩,
+    obtain ⟨n, hn⟩ := h (a.swap : ((<) : ℕ → ℕ → Prop) →r ((<) : α → α → Prop)).to_preorder_hom,
+    exact n.succ_ne_self.symm (rel_embedding.to_preorder_hom_injective _ (hn _ n.le_succ)), },
+end

src/order/preorder_hom.lean

@@ -185,3 +185,26 @@ lemma to_preorder_hom_coe {X Y : Type*} [preorder X] [preorder Y] (f : X ↪o Y)
   (f.to_preorder_hom : X → Y) = (f : X → Y) := rfl
 
 end order_embedding
+section rel_hom
+
+variables {α β : Type*} [partial_order α] [preorder β]
+
+namespace rel_hom
+
+variables (f : ((<) : α → α → Prop) →r ((<) : β → β → Prop))
+
+/-- A bundled expression of the fact that a map between partial orders that is strictly monotonic
+is weakly monotonic. -/
+def to_preorder_hom : α →ₘ β :=
+{ to_fun    := f,
+  monotone' := strict_mono.monotone (λ x y, f.map_rel), }
+
+@[simp] lemma to_preorder_hom_coe_fn : ⇑f.to_preorder_hom = f := rfl
+
+end rel_hom
+
+lemma rel_embedding.to_preorder_hom_injective (f : ((<) : α → α → Prop) ↪r ((<) : β → β → Prop)) :
+  function.injective (f : ((<) : α → α → Prop) →r ((<) : β → β → Prop)).to_preorder_hom :=
+λ _ _ h, f.injective h
+
+end rel_hom