Zulip Chat Archive

Stream: general

Topic: Sup vs sup


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 06 2018 at 05:49):

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

view this post on Zulip Mario Carneiro (Dec 06 2018 at 05:50):

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

view this post on Zulip 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