Stream: new members

Topic: exists distribution over and

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⟩⟩)


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

Mario Carneiro (Nov 20 2020 at 06:40):

the projection ones are just Exists.imp

Mario Carneiro (Nov 20 2020 at 06:41):

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

Last updated: May 11 2021 at 14:11 UTC