[Merged by Bors] - feat(Data/Sum): forall_sum_pi #6658
Conversation
ChrisHughes24
commented
Aug 18, 2023
ChrisHughes24
commented
ChrisHughes24
added
the
awaiting-review
Mathlib/Data/Sum/Basic.lean
Outdated
| @@ -59,6 +59,20 @@ theorem «exists» {p : Sum α β → Prop} : (∃ x, p x) ↔ (∃ a, p (inl a) | |||
| | Or.inr ⟨b, h⟩ => ⟨inr b, h⟩⟩ | |||
| #align sum.exists Sum.exists | |||
|
|
|||
| theorem forall_sum_pi (p : α ⊕ β → Sort*) | |||
| (q : (∀ a, p a) → Prop) : | |||
| (∀ a, q a) ↔ (∀ a b, q (Sum.rec a b)) := | |||
There was a problem hiding this comment.
Can you add the types of a and b here for clarity?
There was a problem hiding this comment.
Or at least, name them more clearly, since the a here is different from the a on the line above, and neither is of type α!
| (∀ a, q a) ↔ (∀ a b, q (Sum.rec a b)) := | |
| (∀ fab, q fab) ↔ (∀ fa fb, q (Sum.rec fa fb)) := |
There was a problem hiding this comment.
done. I also made some arguments implict and improved some other names
| theorem exists_sum_pi {γ : α ⊕ β → Sort*} (p : (∀ ab, γ ab) → Prop) : | ||
| (∃ fab, p fab) ↔ (∃ fa fb, p (Sum.rec fa fb)) := by | ||
| rw [← not_forall_not, forall_sum_pi] | ||
| simp |
There was a problem hiding this comment.
I'm curious if this brings in classical logic, though I don't really care.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
✌️ ChrisHughes24 can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
| @@ -59,6 +59,18 @@ theorem «exists» {p : Sum α β → Prop} : (∃ x, p x) ↔ (∃ a, p (inl a) | |||
| | Or.inr ⟨b, h⟩ => ⟨inr b, h⟩⟩ | |||
| #align sum.exists Sum.exists | |||
|
|
|||
| theorem forall_sum_pi {γ : α ⊕ β → Sort*} (p : (∀ ab, γ ab) → Prop) : | |||
There was a problem hiding this comment.
I think we have a similar lemma for fin tuples; can you check if the naming is consistent?
There was a problem hiding this comment.
Ah, I'm thinking of Fin.forall_fin_succ_pi, which I guess is consistent already.
|
bors r+ |
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
|
Build failed: |
|
bors merge |
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
|
Build failed: |
|
bors r+ |
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
