-
Notifications
You must be signed in to change notification settings - Fork 264
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.
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
[Merged by Bors] - feat port: Data.Set.Pointwise.BigOperators #1651
Closed
Closed
Changes from all commits
Commits
Show all changes
8 commits
Select commit
Hold shift + click to select a range
c10871b
feat: port Data.Set.Pointwise.BigOperators
xroblot 4efc21a
Initial file copy from mathport
xroblot 9624868
Mathbin -> Mathlib; add import to Mathlib.lean
xroblot 473e3e9
First pass
xroblot b6ac2e5
2nd pass
xroblot 548b2ce
Fix last errors
xroblot 3872867
Add align for lemmas generated by to_additive
xroblot 620ee03
Typo
xroblot File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,152 @@ | ||
/- | ||
Copyright (c) 2021 Eric Wieser. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Eric Wieser | ||
|
||
! This file was ported from Lean 3 source module data.set.pointwise.big_operators | ||
! leanprover-community/mathlib commit 008205aa645b3f194c1da47025c5f110c8406eab | ||
! Please do not edit these lines, except to modify the commit id | ||
! if you have ported upstream changes. | ||
-/ | ||
import Mathlib.Algebra.BigOperators.Basic | ||
import Mathlib.Data.Set.Pointwise.Basic | ||
|
||
/-! | ||
# Results about pointwise operations on sets and big operators. | ||
-/ | ||
|
||
|
||
namespace Set | ||
|
||
section BigOperators | ||
|
||
-- Porting note: commented out the next line | ||
-- open BigOperators | ||
|
||
open Pointwise Function | ||
|
||
variable {α : Type _} {ι : Type _} [CommMonoid α] | ||
|
||
/-- The n-ary version of `Set.mem_mul`. -/ | ||
@[to_additive " The n-ary version of `Set.mem_add`. "] | ||
theorem mem_finset_prod (t : Finset ι) (f : ι → Set α) (a : α) : | ||
(a ∈ ∏ i in t, f i) ↔ ∃ (g : ι → α)(_ : ∀ {i}, i ∈ t → g i ∈ f i), (∏ i in t, g i) = a := by | ||
classical | ||
induction' t using Finset.induction_on with i is hi ih generalizing a | ||
· simp_rw [Finset.prod_empty, Set.mem_one] | ||
exact ⟨fun h ↦ ⟨fun _ ↦ a, fun hi ↦ False.elim (Finset.not_mem_empty _ hi), h.symm⟩, | ||
fun ⟨_, _, hf⟩ ↦ hf.symm⟩ | ||
rw [Finset.prod_insert hi, Set.mem_mul] | ||
simp_rw [Finset.prod_insert hi] | ||
simp_rw [ih] | ||
constructor | ||
· rintro ⟨x, y, hx, ⟨g, hg, rfl⟩, rfl⟩ | ||
refine ⟨Function.update g i x, ?_, ?_⟩ | ||
· intro j hj | ||
obtain rfl | hj := Finset.mem_insert.mp hj | ||
· rwa [Function.update_same] | ||
· rw [update_noteq (ne_of_mem_of_not_mem hj hi)] | ||
exact hg hj | ||
· rw [Finset.prod_update_of_not_mem hi, Function.update_same] | ||
· rintro ⟨g, hg, rfl⟩ | ||
exact ⟨g i, is.prod g, hg (is.mem_insert_self _), | ||
⟨⟨g, fun hi ↦ hg (Finset.mem_insert_of_mem hi), rfl⟩, rfl⟩⟩ | ||
#align set.mem_finset_prod Set.mem_finset_prod | ||
#align set.mem_finset_sum Set.mem_finset_sum | ||
|
||
/-- A version of `Set.mem_finset_prod` with a simpler RHS for products over a Fintype. -/ | ||
@[to_additive " A version of `Set.mem_finset_sum` with a simpler RHS for sums over a Fintype. "] | ||
theorem mem_fintype_prod [Fintype ι] (f : ι → Set α) (a : α) : | ||
(a ∈ ∏ i, f i) ↔ ∃ (g : ι → α)(_ : ∀ i, g i ∈ f i), (∏ i, g i) = a := by | ||
rw [mem_finset_prod] | ||
simp | ||
#align set.mem_fintype_prod Set.mem_fintype_prod | ||
#align set.mem_fintype_sum Set.mem_fintype_sum | ||
|
||
/-- An n-ary version of `Set.mul_mem_mul`. -/ | ||
@[to_additive " An n-ary version of `Set.add_mem_add`. "] | ||
theorem list_prod_mem_list_prod (t : List ι) (f : ι → Set α) (g : ι → α) (hg : ∀ i ∈ t, g i ∈ f i) : | ||
(t.map g).prod ∈ (t.map f).prod := by | ||
induction' t with h tl ih | ||
· simp_rw [List.map_nil, List.prod_nil, Set.mem_one] | ||
· simp_rw [List.map_cons, List.prod_cons] | ||
exact mul_mem_mul (hg h <| List.mem_cons_self _ _) | ||
(ih fun i hi ↦ hg i <| List.mem_cons_of_mem _ hi) | ||
#align set.list_prod_mem_list_prod Set.list_prod_mem_list_prod | ||
#align set.list_sum_mem_list_sum Set.list_sum_mem_list_sum | ||
|
||
/-- An n-ary version of `Set.mul_subset_mul`. -/ | ||
@[to_additive " An n-ary version of `Set.add_subset_add`. "] | ||
theorem list_prod_subset_list_prod (t : List ι) (f₁ f₂ : ι → Set α) (hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) : | ||
(t.map f₁).prod ⊆ (t.map f₂).prod := by | ||
induction' t with h tl ih | ||
· rfl | ||
· simp_rw [List.map_cons, List.prod_cons] | ||
exact mul_subset_mul (hf h <| List.mem_cons_self _ _) | ||
(ih fun i hi ↦ hf i <| List.mem_cons_of_mem _ hi) | ||
#align set.list_prod_subset_list_prod Set.list_prod_subset_list_prod | ||
#align set.list_sum_subset_list_sum Set.list_sum_subset_list_sum | ||
|
||
@[to_additive] | ||
theorem list_prod_singleton {M : Type _} [CommMonoid M] (s : List M) : | ||
(s.map fun i ↦ ({i} : Set M)).prod = {s.prod} := | ||
(map_list_prod (singletonMonoidHom : M →* Set M) _).symm | ||
#align set.list_prod_singleton Set.list_prod_singleton | ||
#align set.list_sum_singleton Set.list_sum_singleton | ||
|
||
/-- An n-ary version of `Set.mul_mem_mul`. -/ | ||
@[to_additive " An n-ary version of `Set.add_mem_add`. "] | ||
theorem multiset_prod_mem_multiset_prod (t : Multiset ι) (f : ι → Set α) (g : ι → α) | ||
(hg : ∀ i ∈ t, g i ∈ f i) : (t.map g).prod ∈ (t.map f).prod := by | ||
induction t using Quotient.inductionOn | ||
simp_rw [Multiset.quot_mk_to_coe, Multiset.coe_map, Multiset.coe_prod] | ||
exact list_prod_mem_list_prod _ _ _ hg | ||
#align set.multiset_prod_mem_multiset_prod Set.multiset_prod_mem_multiset_prod | ||
#align set.multiset_sum_mem_multiset_sum Set.multiset_sum_mem_multiset_sum | ||
|
||
/-- An n-ary version of `Set.mul_subset_mul`. -/ | ||
@[to_additive " An n-ary version of `Set.add_subset_add`. "] | ||
theorem multiset_prod_subset_multiset_prod (t : Multiset ι) (f₁ f₂ : ι → Set α) | ||
(hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) : (t.map f₁).prod ⊆ (t.map f₂).prod := by | ||
induction t using Quotient.inductionOn | ||
simp_rw [Multiset.quot_mk_to_coe, Multiset.coe_map, Multiset.coe_prod] | ||
exact list_prod_subset_list_prod _ _ _ hf | ||
#align set.multiset_prod_subset_multiset_prod Set.multiset_prod_subset_multiset_prod | ||
#align set.multiset_sum_subset_multiset_sum Set.multiset_sum_subset_multiset_sum | ||
|
||
@[to_additive] | ||
theorem multiset_prod_singleton {M : Type _} [CommMonoid M] (s : Multiset M) : | ||
(s.map fun i ↦ ({i} : Set M)).prod = {s.prod} := | ||
(map_multiset_prod (singletonMonoidHom : M →* Set M) _).symm | ||
#align set.multiset_prod_singleton Set.multiset_prod_singleton | ||
#align set.multiset_sum_singleton Set.multiset_sum_singleton | ||
|
||
/-- An n-ary version of `Set.mul_mem_mul`. -/ | ||
@[to_additive " An n-ary version of `Set.add_mem_add`. "] | ||
theorem finset_prod_mem_finset_prod (t : Finset ι) (f : ι → Set α) (g : ι → α) | ||
(hg : ∀ i ∈ t, g i ∈ f i) : (∏ i in t, g i) ∈ ∏ i in t, f i := | ||
multiset_prod_mem_multiset_prod _ _ _ hg | ||
#align set.finset_prod_mem_finset_prod Set.finset_prod_mem_finset_prod | ||
#align set.finset_sum_mem_finset_sum Set.finset_sum_mem_finset_sum | ||
|
||
/-- An n-ary version of `Set.mul_subset_mul`. -/ | ||
@[to_additive " An n-ary version of `Set.add_subset_add`. "] | ||
theorem finset_prod_subset_finset_prod (t : Finset ι) (f₁ f₂ : ι → Set α) | ||
(hf : ∀ i ∈ t, f₁ i ⊆ f₂ i) : (∏ i in t, f₁ i) ⊆ ∏ i in t, f₂ i := | ||
multiset_prod_subset_multiset_prod _ _ _ hf | ||
#align set.finset_prod_subset_finset_prod Set.finset_prod_subset_finset_prod | ||
#align set.finset_sum_subset_finset_sum Set.finset_sum_subset_finset_sum | ||
|
||
@[to_additive] | ||
theorem finset_prod_singleton {M ι : Type _} [CommMonoid M] (s : Finset ι) (I : ι → M) : | ||
(∏ i : ι in s, ({I i} : Set M)) = {∏ i : ι in s, I i} := | ||
(map_prod (singletonMonoidHom : M →* Set M) _ _).symm | ||
#align set.finset_prod_singleton Set.finset_prod_singleton | ||
#align set.finset_sum_singleton Set.finset_sum_singleton | ||
|
||
/-! TODO: define `decidable_mem_finset_prod` and `decidable_mem_finset_sum`. -/ | ||
|
||
|
||
end BigOperators | ||
|
||
end Set |
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Corresponding align tags have to be added for the theorems generated by
to_additive
. (If you're not sure what they are, you can replaceto_additive
byto_additive?
and see what it outputs.)There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the review.
I have added the
align
for the lemmas generated byto_additive
. I did not do that in my previous PR. So I wonder why is it necessary to do it for this one? Is it because they cannot be auto-generated for some reason?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It was also necessary in previous PRs, it's just very easy to overlook :-) There are more details in the porting wiki, there's a whole section about
to_additive
.