Zulip Chat Archive
Stream: new members
Topic: WithBot lemma
Sayantan Santra (Jun 15 2023 at 22:00):
Could anyone help me prove the following?
import Mathlib.Order.WithBot
lemma foo [PartialOrder α] [OrderBot α] {a : WithBot α} (h : a < (⊥ : α)) : a = ⊥ := by
sorry
Yaël Dillies (Jun 15 2023 at 22:02):
(untested)
by
cases a
. rfl
. cases h.not_le (WithBot.coe_le_coe.2 bot_le)
Sayantan Santra (Jun 15 2023 at 22:10):
@Yaël Dillies Thank you so much.
Eric Wieser (Jun 15 2023 at 22:29):
Do we not have a lemma like docs#lt_bot?
Last updated: Dec 20 2023 at 11:08 UTC