sup_eq_max

Stream: general

[Chris Hughes]

Is there a nice way to state the lemma a ⊔ b = max a b, in general, for when sup is not derived from max such as on with_bot, or do I just have to prove it for with_bot

[Mario Carneiro]

You can prove sup a b = max a b on any type for which max makes sense

[Mario Carneiro]

Oh, I see... There are two lattice structures on with_bot that don't coincide by defeq

[Mario Carneiro]

but they are the same since they have the same le

[Mario Carneiro]

unfortunately, despite how I've said that non-defeq diamonds are evil and should be avoided, there is not much I can do about this one since it would require adding a sup field to decidable_linear_order which is in core

[Chris Hughes]

It makes sense to add this lemma then?

lemma sup_eq_max [decidable_linear_order α] (a b : with_bot α) : a ⊔ b = max a b :=
le_antisymm (sup_le (le_max_left _ _) (le_max_right _ _)) (max_le le_sup_left le_sup_right)

[Johan Commelin]

/me thinks that core shouldn't be in core

[Chris Hughes]

Why did that message appear next to your name instead of beneath?

[Kevin Buzzard]

because he only thought it, he didn't post it

[Kevin Buzzard]

There are rumours that core won't be in core in Lean 4

[Johan Commelin]

Why did that message appear next to your name instead of beneath?

Yeah, I'm old. My IRC habits betray me. (Hint: type /me before your message.)