SemilatticeInf as a hypothesis

Stream: mathlib4

[Wrenna Robson]

Suppose you have a type with an existing LE on it - Subtype p when there's an ambient relation is a good example - and you want to assert as a hypothesis "SemilatticeInf (Subtype p)" - but you want the LE for that to be the one that already exists, to avoid diamond issues. How do you specify that?

[Wrenna Robson]

I guess in general my question is like, why do the classes for orders mix data and propositions in this way.

[Aaron Liu]

Just don't

[Aaron Liu]

How about ∀ a b, ∃ c, IsGLB {a, b} c

[Wrenna Robson]

Oh, sure, if that's a preferred spelling

[Aaron Liu]

I haven't seen it used anywhere

[Wrenna Robson]

I guess what I don't quite get, design-wise, is why OrderBot instead has [LE _] as a required instance

[Aaron Liu]

but it seems better than putting an unrelated SemilatticeInf on you type and then asserting a compatibility

[Wrenna Robson]

While SemilatticeInf doesn't do that.

[Wrenna Robson]

It seems inconsistent to me but I feel like it's more likely I'm missing something subtlety.

[Wrenna Robson]

@Yaël Dillies I assume you'll know why it's designed like this.

[Yaël Dillies]

Wrenna Robson said:

How do you specify that?

You use SubsemilatticeSup, the missing SemilatticeSup counterpart to docs#Sublattice

[Wrenna Robson]

Ah.