Unknown mathematical structure

Stream: general

[Alistair Tucker]

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]

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]

What drives you to investigate this particular combination of axioms?

[Alistair Tucker]

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

[Mario Carneiro]

One random observation I can make is that r doesn't need to have the same domain and codomain

[Mario Carneiro]

although q needs it

[Mario Carneiro]

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

[Alistair Tucker]

I'm not sure what you mean by a different domain and codomain of r. Something like r : α → β → Prop?

[Mario Carneiro]

yeah

[Alistair Tucker]

Sorry I'm not a real mathematician :)

[Mario Carneiro]

also A doesn't need a bottom

[Eric Wieser]

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

[Eric Wieser]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

The first two axioms say that for each fixed a, r a is a sub-sup_bot_semilattice

[Mario Carneiro]

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