## 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?

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