Zulip Chat Archive

Stream: new members

Topic: exists distribution over and


view this post on Zulip Yakov Pechersky (Nov 20 2020 at 01:36):

What's the mathlib name for this lemma and the ones that only retain the left or right branch?

example {α : Type*} {p q : α  Prop} (h :  x, p x  q x) : ( x, p x)  ( x, q x) :=
exists.elim h (λ x P, Q⟩, ⟨⟨x, P⟩, x, Q⟩⟩)

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 06:26):

You can probably find it in logic.basic or with library_search but I'm guessing exists_and_distrib. I don't know about the projection ones though

view this post on Zulip Mario Carneiro (Nov 20 2020 at 06:40):

the projection ones are just Exists.imp

view this post on Zulip Mario Carneiro (Nov 20 2020 at 06:41):

like Exists.imp (\lam _, and.left)


Last updated: May 11 2021 at 14:11 UTC