# Zulip Chat Archive

## Stream: general

### Topic: Unknown mathematical structure

#### Alistair Tucker (Feb 23 2021 at 09:21):

Hello everyone. Thank you all for working so hard on this amazing project!

I have defined an inductive type

```
import order.bounded_lattice
variables {α : Type*} [semilattice_sup_bot α]
inductive q (r : α → α → Prop) : α → Prop
| base : q ⊥
| succ (b c : α) : c < b → r c b → q c → q b
```

depending on a relation `r`

satisfying the following axioms:

```
variable {r : α → α → Prop}
variable hr₀ : r ⊥ ⊥
variable hr₁ (b c d : α) : d ≤ c → r d b → r c b
variable hr₂ (b c d : α) : r d b → r d c → r d (b ⊔ c)
```

Here are some examples of properties that derive from the axioms:

```
lemma hr₄ {b : α} : q r b → r b b
lemma hr₅ {b c d : α} : r d c → q r b → r (b ⊔ d) (b ⊔ c)
lemma hr₆ {b c : α} : q r b → q r c → q r (b ⊔ c)
lemma hr₈ {a : α} : q r a → ∀ c < a, q r c → ∃ b, c ≤ b ∧ b < a ∧ q r b ∧ r b a
```

#### Alistair Tucker (Feb 23 2021 at 09:21):

My question is, is there a better way to express this by using the machinery of mathlib? I can prove all these various things by hand but I don't have a name for this structure and I wonder if I'm reinventing the wheel...

#### Mario Carneiro (Feb 23 2021 at 09:23):

What drives you to investigate this particular combination of axioms?

#### Alistair Tucker (Feb 23 2021 at 09:24):

It' s supposed to model the relationships among a particular set of partial differential equations :)

#### Mario Carneiro (Feb 23 2021 at 09:25):

One random observation I can make is that `r`

doesn't need to have the same domain and codomain

#### Mario Carneiro (Feb 23 2021 at 09:26):

although `q`

needs it

#### Mario Carneiro (Feb 23 2021 at 09:27):

I think you would be best served just making up some name for this and working with it for a while

#### Alistair Tucker (Feb 23 2021 at 09:29):

I'm not sure what you mean by a different domain and codomain of `r`

. Something like `r : α → β → Prop`

?

#### Mario Carneiro (Feb 23 2021 at 09:29):

yeah

#### Alistair Tucker (Feb 23 2021 at 09:29):

Sorry I'm not a real mathematician :)

#### Mario Carneiro (Feb 23 2021 at 09:29):

also A doesn't need a bottom

#### Eric Wieser (Feb 23 2021 at 09:30):

I don't see how your generalization works Mario, can you paste the code?

#### Eric Wieser (Feb 23 2021 at 09:31):

`q b -> q c`

requires b and c to be the same type, right?

#### Mario Carneiro (Feb 23 2021 at 09:35):

```
import order.bounded_lattice
structure tuckerian {α β} [preorder α] [semilattice_sup_bot β] (r : α → β → Prop) : Prop :=
(bottom : ∀ a, r a ⊥)
(sup : ∀ (a : α) (b c : β), r a b → r a c → r a (b ⊔ c))
(downward_closed : ∀ a b : α, a ≤ b → ∀ c : β, r b c → r a c)
inductive tuckerian_closure {α} [semilattice_sup_bot α] (r : α → α → Prop) : α → Prop
| base : tuckerian_closure ⊥
| succ (b c : α) : c < b → r c b → tuckerian_closure c → tuckerian_closure b
```

#### Alistair Tucker (Feb 23 2021 at 09:36):

Wow! I always wanted something named after me :) Thank you very much

#### Mario Carneiro (Feb 23 2021 at 09:36):

The first two axioms say that for each fixed `a`

, `r a`

is a sub-`sup_bot_semilattice`

#### Mario Carneiro (Feb 23 2021 at 09:38):

so this is an antitone function from `A -> sup_bot_subsemilattice B`

Last updated: May 12 2021 at 03:23 UTC