Zulip Chat Archive

Stream: Is there code for X?

Topic: exists simplifying ors


view this post on Zulip Yakov Pechersky (Apr 08 2021 at 07:23):

Do we have these?

@[simp] lemma exists_or_eq_left {α : Sort*} (y : α) (p : α  Prop) :  (x : α), x = y  p x :=
y, or.inl rfl

@[simp] lemma exists_or_eq_right {α : Sort*} (y : α) (p : α  Prop) :  (x : α), p x  x = y :=
y, or.inr rfl

view this post on Zulip Eric Wieser (Apr 08 2021 at 07:31):

I assume we have docs#exist_eq?

view this post on Zulip Eric Wieser (Apr 08 2021 at 07:31):

But I guess not under that name...


Last updated: May 07 2021 at 19:12 UTC