Zulip Chat Archive
Stream: Is there code for X?
Topic: Prod.Lex
Kim Morrison (Dec 21 2023 at 07:06):
Is
theorem Prod.Lex_iff {x w : α} {y z : β} :
Prod.Lex r s (x, y) (w, z) = (r x w ∨ x = w ∧ s y z) := ...
somewhere? Surely I am just failing to find it!
Yaël Dillies (Dec 21 2023 at 07:08):
Kim Morrison (Dec 21 2023 at 07:09):
Ah, was looking in Std.
Kim Morrison (Dec 21 2023 at 07:18):
It will be there soon, I guess. :-)
Last updated: May 02 2025 at 03:31 UTC