…15399)

# Well-founded typeclasses

We introduce a new unbundled typeclass `is_well_founded` for a general well-founded relation, and reducible defs `well_founded_lt` and `well_founded_gt` for well-founded `<` and `>` specifically, to be used as mixins. For now, all we do is specialize only the most basic API on well-founded relations to these new typeclasses. 

This is just an initial development. If this is merged, a subsequent PR will redefine `is_well_order` in terms of `is_well_founded` (and remove the redundant `irrefl` field). Further PRs will focus on providing all the possible instances for this new typeclass, and actually using it throughout mathlib.

Moved from #15023. 

## Why do we want this?

Here's the part where I justify why this is a good thing we want in mathlib.

### Well-ordered `<`

There is a need to talk about well-ordered `<` relations, as a quick search for `is_well_order α (<)` or `is_well_order ι (<)` reveals. The most obvious way to spell this condition out, namely `[has_lt α] [is_well_order α (<)]` is actually the most inconvenient, since none of the results for linear orders are available. You actually need to write `[linear_order α] [is_well_order α (<)]` instead.

With this new typeclass, the obvious spelling is now the good one: `[linear_order α] [well_founded_lt α]`

### Redundant typeclasses

We actually already at least four typeclasses for the well-foundedness of a concrete relation: `category.noetherian_object`, `category.artinian_object`, `topological_space.noetherian_space`, and `wf_dvd_monoid`. One currently needs to specialize the characterizing properties of a well-founded relation to these separate typeclasses in order to use them. Redefining these typeclasses in terms of these new ones, and making them `reducible def`s, would alleviate this problem.

### Typeclass inference

Well-founded relations are actually a nice candidate for typeclass inference, since there's many common constructions that automatically preserve well-foundedness. These include taking inverse images (including `measure` and `order.preimage`), maps through relation embeddings (including subtypes), lexicographic sums or products, and adding a top or bottom element. Many of these are currently provided as instances, but only for well-orders.

### Misleading theorem names 

Perhaps the most useful result on well-founded relations is that every nonempty set has a minimum - when you view the relation as `<`, that is. This leads to misleading theorem names when you're using them on a well-founded `>` relation. With this refactor, we could simply specialize `well_founded.min` into `well_founded_gt.max` and end up with clearer theorem statements.

On a related note, given a linear order and a well-founded `<` relation, we can rephrase `well_founded.not_lt_min` into the much more convenient `well_founded_lt.min_le`.

…eanprover-community#15399)

# Well-founded typeclasses

We introduce a new unbundled typeclass `is_well_founded` for a general well-founded relation, and reducible defs `well_founded_lt` and `well_founded_gt` for well-founded `<` and `>` specifically, to be used as mixins. For now, all we do is specialize only the most basic API on well-founded relations to these new typeclasses. 

This is just an initial development. If this is merged, a subsequent PR will redefine `is_well_order` in terms of `is_well_founded` (and remove the redundant `irrefl` field). Further PRs will focus on providing all the possible instances for this new typeclass, and actually using it throughout mathlib.

Moved from leanprover-community#15023. 

## Why do we want this?

Here's the part where I justify why this is a good thing we want in mathlib.

### Well-ordered `<`

There is a need to talk about well-ordered `<` relations, as a quick search for `is_well_order α (<)` or `is_well_order ι (<)` reveals. The most obvious way to spell this condition out, namely `[has_lt α] [is_well_order α (<)]` is actually the most inconvenient, since none of the results for linear orders are available. You actually need to write `[linear_order α] [is_well_order α (<)]` instead.

With this new typeclass, the obvious spelling is now the good one: `[linear_order α] [well_founded_lt α]`

### Redundant typeclasses

We actually already at least four typeclasses for the well-foundedness of a concrete relation: `category.noetherian_object`, `category.artinian_object`, `topological_space.noetherian_space`, and `wf_dvd_monoid`. One currently needs to specialize the characterizing properties of a well-founded relation to these separate typeclasses in order to use them. Redefining these typeclasses in terms of these new ones, and making them `reducible def`s, would alleviate this problem.

### Typeclass inference

Well-founded relations are actually a nice candidate for typeclass inference, since there's many common constructions that automatically preserve well-foundedness. These include taking inverse images (including `measure` and `order.preimage`), maps through relation embeddings (including subtypes), lexicographic sums or products, and adding a top or bottom element. Many of these are currently provided as instances, but only for well-orders.

### Misleading theorem names 

Perhaps the most useful result on well-founded relations is that every nonempty set has a minimum - when you view the relation as `<`, that is. This leads to misleading theorem names when you're using them on a well-founded `>` relation. With this refactor, we could simply specialize `well_founded.min` into `well_founded_gt.max` and end up with clearer theorem statements.

On a related note, given a linear order and a well-founded `<` relation, we can rephrase `well_founded.not_lt_min` into the much more convenient `well_founded_lt.min_le`.

…15399)

# Well-founded typeclasses

We introduce a new unbundled typeclass `is_well_founded` for a general well-founded relation, and reducible defs `well_founded_lt` and `well_founded_gt` for well-founded `<` and `>` specifically, to be used as mixins. For now, all we do is specialize only the most basic API on well-founded relations to these new typeclasses. 

This is just an initial development. If this is merged, a subsequent PR will redefine `is_well_order` in terms of `is_well_founded` (and remove the redundant `irrefl` field). Further PRs will focus on providing all the possible instances for this new typeclass, and actually using it throughout mathlib.

Moved from #15023. 

## Why do we want this?

Here's the part where I justify why this is a good thing we want in mathlib.

### Well-ordered `<`

There is a need to talk about well-ordered `<` relations, as a quick search for `is_well_order α (<)` or `is_well_order ι (<)` reveals. The most obvious way to spell this condition out, namely `[has_lt α] [is_well_order α (<)]` is actually the most inconvenient, since none of the results for linear orders are available. You actually need to write `[linear_order α] [is_well_order α (<)]` instead.

With this new typeclass, the obvious spelling is now the good one: `[linear_order α] [well_founded_lt α]`

### Redundant typeclasses

We actually already at least four typeclasses for the well-foundedness of a concrete relation: `category.noetherian_object`, `category.artinian_object`, `topological_space.noetherian_space`, and `wf_dvd_monoid`. One currently needs to specialize the characterizing properties of a well-founded relation to these separate typeclasses in order to use them. Redefining these typeclasses in terms of these new ones, and making them `reducible def`s, would alleviate this problem.

### Typeclass inference

Well-founded relations are actually a nice candidate for typeclass inference, since there's many common constructions that automatically preserve well-foundedness. These include taking inverse images (including `measure` and `order.preimage`), maps through relation embeddings (including subtypes), lexicographic sums or products, and adding a top or bottom element. Many of these are currently provided as instances, but only for well-orders.

### Misleading theorem names 

Perhaps the most useful result on well-founded relations is that every nonempty set has a minimum - when you view the relation as `<`, that is. This leads to misleading theorem names when you're using them on a well-founded `>` relation. With this refactor, we could simply specialize `well_founded.min` into `well_founded_gt.max` and end up with clearer theorem statements.

On a related note, given a linear order and a well-founded `<` relation, we can rephrase `well_founded.not_lt_min` into the much more convenient `well_founded_lt.min_le`.

…15399)

# Well-founded typeclasses

We introduce a new unbundled typeclass `is_well_founded` for a general well-founded relation, and reducible defs `well_founded_lt` and `well_founded_gt` for well-founded `<` and `>` specifically, to be used as mixins. For now, all we do is specialize only the most basic API on well-founded relations to these new typeclasses. 

This is just an initial development. If this is merged, a subsequent PR will redefine `is_well_order` in terms of `is_well_founded` (and remove the redundant `irrefl` field). Further PRs will focus on providing all the possible instances for this new typeclass, and actually using it throughout mathlib.

Moved from #15023. 

## Why do we want this?

Here's the part where I justify why this is a good thing we want in mathlib.

### Well-ordered `<`

There is a need to talk about well-ordered `<` relations, as a quick search for `is_well_order α (<)` or `is_well_order ι (<)` reveals. The most obvious way to spell this condition out, namely `[has_lt α] [is_well_order α (<)]` is actually the most inconvenient, since none of the results for linear orders are available. You actually need to write `[linear_order α] [is_well_order α (<)]` instead.

With this new typeclass, the obvious spelling is now the good one: `[linear_order α] [well_founded_lt α]`

### Redundant typeclasses

We actually already at least four typeclasses for the well-foundedness of a concrete relation: `category.noetherian_object`, `category.artinian_object`, `topological_space.noetherian_space`, and `wf_dvd_monoid`. One currently needs to specialize the characterizing properties of a well-founded relation to these separate typeclasses in order to use them. Redefining these typeclasses in terms of these new ones, and making them `reducible def`s, would alleviate this problem.

### Typeclass inference

Well-founded relations are actually a nice candidate for typeclass inference, since there's many common constructions that automatically preserve well-foundedness. These include taking inverse images (including `measure` and `order.preimage`), maps through relation embeddings (including subtypes), lexicographic sums or products, and adding a top or bottom element. Many of these are currently provided as instances, but only for well-orders.

### Misleading theorem names 

Perhaps the most useful result on well-founded relations is that every nonempty set has a minimum - when you view the relation as `<`, that is. This leads to misleading theorem names when you're using them on a well-founded `>` relation. With this refactor, we could simply specialize `well_founded.min` into `well_founded_gt.max` and end up with clearer theorem statements.

On a related note, given a linear order and a well-founded `<` relation, we can rephrase `well_founded.not_lt_min` into the much more convenient `well_founded_lt.min_le`.