Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(Data/Sum): forall_sum_pi #6658

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - feat(Data/Sum): forall_sum_pi #6658

Changes from 2 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
f6b0e98
feat(Data/Sum): forall_sum_pi
ChrisHughes24 Aug 18, 2023
43411c0
use variables for types
ChrisHughes24 Aug 18, 2023
7d222ea
eric's comments
ChrisHughes24 Aug 18, 2023
b24c589
use implicit arguments
ChrisHughes24 Aug 18, 2023
cb0d16d
better naming
ChrisHughes24 Aug 18, 2023
1e645d2
Update Mathlib/Data/Sum/Basic.lean
ChrisHughes24 Aug 18, 2023
caa2ff0
Merge remote-tracking branch 'origin/master' into sumForallChris
ChrisHughes24 Aug 18, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 14 additions & 0 deletions Mathlib/Data/Sum/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)) :=
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you add the types of a and b here for clarity?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 α!

Suggested change
(∀ a, q a) ↔ (∀ a b, q (Sum.rec a b)) :=
(∀ fab, q fab) ↔ (∀ fa fb, q (Sum.rec fa fb)) :=

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done. I also made some arguments implict and improved some other names

⟨fun h a b => h _, fun h a => by
have h1 : a = Sum.rec (fun i => a (Sum.inl i)) (fun i => a (Sum.inr i)) := by
ext b; cases b <;> rfl
rw [h1]; exact h _ _⟩

theorem exists_sum_pi (p : α ⊕ β → Sort*)
(q : (∀ a, p a) → Prop) :
(∃ a, q a) ↔ (∃ a b, q (Sum.rec a b)) := by
rw [← not_forall_not, forall_sum_pi]
simp

theorem inl_injective : Function.Injective (inl : α → Sum α β) := fun _ _ ↦ inl.inj
#align sum.inl_injective Sum.inl_injective

Expand Down
Loading