Zulip Chat Archive
Stream: general
Topic: le_max_left_of_le
Yaël Dillies (Jun 08 2021 at 18:16):
Dumb question, why is lemma le_max_left_of_le : a ≤ b → a ≤ max b c := le_sup_left_of_le not named le_max_of_le_left? It would match other lemmas like le_of_max_le_right.
Yaël Dillies (Jun 08 2021 at 18:16):
The question extends to le_sup_left_of_le.
Anne Baanen (Jun 08 2021 at 19:19):
Anne Baanen (Jun 08 2021 at 19:21):
Probably just because it's very old, and the naming conventions hadn't been applied (as much) yet. I'm in favour of renaming it as you suggest.
Yaël Dillies (Jun 08 2021 at 19:22):
Okay great :)
Yaël Dillies (Jun 08 2021 at 19:22):
Shall I also rename le_sup_left_of_le and similar?
Yaël Dillies (Jun 09 2021 at 07:57):
Yaël Dillies (Jun 09 2021 at 07:58):
(I should really go to my exams, now :stuck_out_tongue:)
Eric Wieser (Jun 09 2021 at 08:17):
(deleted)
Last updated: Dec 20 2023 at 11:08 UTC