# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Ascending chain conditions

#### Oliver Nash (Dec 18 2020 at 22:45):

I need to use an "ascending chain condition". Poking around, I see we have a large body of excellent stuff on orders so I'm a bit surprised that we seem to have everything except how I usually think about this. Do we have anything like `wf_iff_satisfies_acc`

somewhere:

```
import order.well_founded
import order.preorder_hom
import order.order_iso_nat
/-- I see we have `rel_embedding.well_founded_iff_no_descending_seq` but can we have this too?
Can we at least have a comment including the phrase "ascending chain" somewhere? -/
def satisfies_acc (α : Type*) [partial_order α] := ∀ (a : ℕ →ₘ α), ∃ n, ∀ m, n ≤ m → a n = a m
/-- So that we could then add this. Or does this already exists and I can't find it? -/
lemma wf_iff_satisfies_acc (α : Type*) [partial_order α] :
well_founded ((>) : α → α → Prop) ↔ satisfies_acc α := sorry
```

#### Oliver Nash (Dec 18 2020 at 22:47):

In addition, do we have anything along the lines of these (which I need):

```
/-- Do we already have this? Is it sufficiently more useful than `inv_image.wf` to introduce? -/
lemma well_founded_of_embedding {α β : Type*} [partial_order α] [partial_order β]
(f : α →ₘ β) (hf : function.injective f) (h : well_founded ((>) : β → β → Prop)) :
well_founded ((>) : α → α → Prop) := sorry
/-- Surely this property has an "official" name; what is it? -/
def is_sup_compact (α : Type*) [complete_lattice α] :=
∀ (s : set α) (h : s.nonempty), (∀ a b, a ∈ s → b ∈ s → a ⊔ b ∈ s) → (Sup s) ∈ s
/-- Do we already have this? -/
lemma is_sup_compact_of_wf {α : Type*} [complete_lattice α] (h : well_founded ((>) : α → α → Prop)) :
is_sup_compact α := sorry
```

#### Johan Commelin (Dec 19 2020 at 06:06):

I think @Aaron Anderson did some things in this direction a while ago

#### Oliver Nash (Dec 19 2020 at 11:37):

Thanks, maybe I'll see if I can turn some of this into a PR and ping him on that.

#### Oliver Nash (Dec 19 2020 at 13:57):

PR 1 of 2 https://github.com/leanprover-community/mathlib/pull/5434

#### Johan Commelin (Dec 19 2020 at 14:23):

@Aaron Anderson @Mario Carneiro could you mind taking a look at :up: ?

#### Oliver Nash (Dec 19 2020 at 17:38):

I now have (disgusting) proofs of the above modulo the following two results:

```
variables {α}
lemma Sup_sup_Sup_eq_Sup_union
{s t : set α} (hs : s.finite) (ht : t.finite) : Sup s ⊔ Sup t = Sup (s ∪ t) := sorry
lemma finite_Sup_mem {s : set α} (h : s.finite) : Sup s ∈ s := sorry
```

I don't suppose we have these somewhere?

#### Kevin Buzzard (Dec 19 2020 at 17:42):

What are the assumptions on the order?

#### Oliver Nash (Dec 19 2020 at 17:42):

In this case, `complete_lattice`

.

#### Kevin Buzzard (Dec 19 2020 at 17:42):

Isn't subsets of a set a complete lattice?

#### Oliver Nash (Dec 19 2020 at 17:42):

My code snippets are supposed to flow into each other but it's possible I've screwed up.

#### Oliver Nash (Dec 19 2020 at 17:43):

Hmm, am I being dense?

#### Kevin Buzzard (Dec 19 2020 at 17:43):

I think finite_Sup_mem is false for subsets of a set

#### Kevin Buzzard (Dec 19 2020 at 17:43):

Union of two sets might not be either one

#### Oliver Nash (Dec 19 2020 at 17:44):

Oh sorry, I am being dense.

#### Oliver Nash (Dec 19 2020 at 17:44):

Thanks, no wonder this was such a useful lemma!

#### Oliver Nash (Dec 19 2020 at 17:44):

Right, I'm done for the day but I'll pick this up tomorrow. Apologies for the nonsense.

#### Kevin Buzzard (Dec 19 2020 at 17:44):

True for total orders

#### Adam Topaz (Dec 19 2020 at 17:53):

I think `is_sup_compact`

needs some additional assumptions too, e.g. it's false for the set of finite subsets of a type. Edit: ignore this --- just saw it was a `def`

:rofl:

#### Aaron Anderson (Dec 19 2020 at 17:54):

Looking at the PR, it looks like there is quite a bit of work to do in uniting `preorder_hom`

and `rel_hom`

.

#### Oliver Nash (Dec 19 2020 at 17:57):

I'm confident the only outright error is the one Kevin identified since I have sorry-free proofs of everything except `is_sup_compact_iff`

(which I actually don't even need).

#### Oliver Nash (Dec 19 2020 at 17:58):

Aaron Anderson said:

Looking at the PR, it looks like there is quite a bit of work to do in uniting

`preorder_hom`

and`rel_hom`

.

Yes, there seem to be basically no bridges between these two except the tiny scraps I have introduced.

#### Aaron Anderson (Dec 19 2020 at 17:59):

There's also work that you should look at in `order_iso_nat`

#### Oliver Nash (Dec 19 2020 at 18:00):

You mean the file `order_iso_nat.lean`

?

#### Aaron Anderson (Dec 19 2020 at 18:00):

Yes

#### Aaron Anderson (Dec 19 2020 at 18:00):

which proves well-founded iff no strictly-ascending-chains

#### Oliver Nash (Dec 19 2020 at 18:01):

Yes, I actually used that.

#### Oliver Nash (Dec 19 2020 at 18:01):

#### Aaron Anderson (Dec 19 2020 at 18:01):

I see

#### Oliver Nash (Dec 19 2020 at 18:02):

Darn, gotta run. Visitors arrived. Apologies.

#### Aaron Anderson (Dec 19 2020 at 18:04):

We should fill out the connections between `preorder_hom`

and `rel_hom`

, or else refactor `preorder_hom`

to use `rel_hom`

and porting the `preorder_hom`

API to that new definition, but I'm ok with getting a PR or two on ACC and DCC first.

#### Aaron Anderson (Dec 19 2020 at 18:09):

I would probably guess that ACC and DCC should be instances you can place on a `partial_order`

rather than just props

#### Aaron Anderson (Dec 19 2020 at 18:10):

and you can define DCC either through using a different kind of `rel_hom`

in the definition, or just ACC of the order dual.

#### Oliver Nash (Dec 20 2020 at 17:11):

I now have a second PR here with some of the other results I'd like to use: https://github.com/leanprover-community/mathlib/pull/5446

The proofs are a total mess and so should be ignored (though this time they have the advantage of not requiring any `false`

lemmas). However I would be grateful for feedback on whether it looks like I'm taking things in a useful direction in terms of what I'm defining and proving.

Unfortunately as usual I'm in a hurry and must now run off but I will have some time tomorrow and will pay careful attention to any remarks others may have to offer.

#### Oliver Nash (Apr 06 2021 at 20:06):

Since I now want to use the result, I've decided to revive this previously-abandoned PR: https://github.com/leanprover-community/mathlib/pull/5434

#### Johan Commelin (Apr 06 2021 at 20:07):

Good luck! :happy:

#### Oliver Nash (Apr 06 2021 at 20:07):

Thanks :D

#### Oliver Nash (Apr 06 2021 at 20:07):

I'm afraid I rebased rather than merged master to resolve a merge conflict so I've blown away the branch history but what I understood to be the most contentious issue was the new typeclass which I have removed.

Last updated: May 17 2021 at 15:13 UTC