GeneralizedBooleanAlgebra and ConditionallyComplete diamond

Stream: mathlib4

[Robert Maxton]

import Mathlib.Order.BooleanAlgebra.Basic
import Mathlib.Logic.Pairwise
import Mathlib.Order.ConditionallyCompleteLattice.Defs

example {α ι : Type*} [GeneralizedBooleanAlgebra α] [ConditionallyCompleteLattice α]
    (f : ι → α) (hf : Pairwise (Function.onFun Disjoint f)) -- failed to synthesize OrderBot α
    (i : ι ) : True := by trivial

I'm looking for a spelling that lets me work with relative complements and indexed suprema at the same time; what's the best way to do that? For right now I'm manually providing GeneralizedBooleanAlgebra.toOrderBot as an explicit argument to Disjoint, but I imagine that's just buying trouble...

[Aaron Liu]

yeah that's a diamond

[Aaron Liu]

don't have the diamond

[Robert Maxton]

yeah, but how :p

[Aaron Liu]

do you have an order top?

[Robert Maxton]

... I could make that assumption, I suppose, though I'd kind of prefer not to.
More to the point, tho, that only kicks the can down the road: BooleanAlgebra and CompleteLattice still give me diamond problems later.

[Aaron Liu]

I'm thinking about docs#Order.Coframe

[Robert Maxton]

mmmm

[Aaron Liu]

I don't think the specific case of conditionally complete order + relative complements is in mathlib

[Aaron Liu]

without a top

[Robert Maxton]

bleh.
Alright, I'll just stick with CompleteBooleanAlgebra now that I've found it

[Aaron Liu]

but with a top I think this might be exactly docs#Order.Coframe

[Robert Maxton]

hmm

[Robert Maxton]

Coframe looks approximately correct

[Robert Maxton]

I'll give it a shot and see what happens
Thanks!

[Yury G. Kudryashov]

Another option is to define a class (in your project) that extends both.