## Stream: general

### Topic: Sup vs sup

#### Johan Commelin (Dec 06 2018 at 05:46):

Is there something in mathlib expressing compatibility between Sup and sup for complete lattices?
I would expect something like

lemma Sup_eq_sup (a b : X) : Sup {x | x = a \or x = b} = a \sqcup b := sorry


#### Mario Carneiro (Dec 06 2018 at 05:49):

that's Sup {a, b} on the left, did you look for that?

#### Mario Carneiro (Dec 06 2018 at 05:50):

also it might be expressed in terms of Sup (insert a s)

#### Johan Commelin (Dec 06 2018 at 05:51):

Aah, there is a Sup_insert. And that can be chained with Sup_singleton

Last updated: May 08 2021 at 18:17 UTC