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