pi boolean algebra

Stream: Is there code for X?

[Heather Macbeth]

Is this true? It's not true by rfl, and library_search doesn't find it with minimal imports.

import data.set.lattice

variables {X : Type*}

example :
  (pi.complete_boolean_algebra : complete_boolean_algebra (set X)) = set.complete_boolean_algebra :=
sorry

[Heather Macbeth]

(@Bryan Gin-ge Chen maybe?)

[Johan Commelin]

The projection onto Sup isn't rfl either:

example :
  (pi.complete_boolean_algebra : complete_boolean_algebra (set X)).Sup =
 set.complete_boolean_algebra.Sup := rfl -- fails

[Heather Macbeth]

Seemingly le, sup and inf agree; Sup and Inf don't.

[Reid Barton]

If they have the same le and they are both partial orders then the rest of the operations must be equal because they are determined by universal properties. (For $\neg$, we have $x \le \neg y \iff x \sqcap y \le \bot$.)

[Reid Barton]

Also I see that a boolean_algebra is already a poset by definition, so you can ignore that condition.