[Merged by Bors] - refactor(data/set/pairwise): Indexed sets as arguments to `set.pairwise_disjoint` #9898

YaelDillies · 2021-10-23T08:43:53Z

This will allow to express the bind operation: you can't currently express that the pairwise disjoint union of pairwise disjoint sets pairwise disjoint. Here's the corresponding statement with finset.sup_indep (defined in #9867):

lemma sup_indep.sup {s : finset ι'} {g : ι' → finset ι} {f : ι → α}
  (hs : s.sup_indep (λ i, (g i).sup f)) (hg : ∀ i' ∈ s, (g i').sup_indep f) :
  (s.sup g).sup_indep f :=

You currently can't do set.pairwise_disjoint s (λ i, ⋃ x ∈ g i, f x).

src/data/set/pairwise.lean

eric-wieser · 2021-10-23T09:26:38Z

Can you expand a little upon the motivation in the PR description? The fact this introduces a bunch of ids in downstream uses makes it not so obviously an improvement to me.

src/data/set/pairwise.lean

YaelDillies · 2021-10-23T11:25:29Z

What do you think about it now? The fact that I had to add a bunch of id is misleading: All current uses of set.pairwise_disjoint were constrained by the fact you needed to use id, so me adding a bunch of them is expected. Note however that some lemmas do require the generalization I'm providing here, finset.prod_bUnion for example.

jcommelin · 2021-10-25T11:49:01Z

@YaelDillies I think Eric's point is that the ids are now explicit. I understand that you are generalizing an existing thing. Should there be a wrapper for the old definition that hides the ids?

YaelDillies · 2021-10-25T13:12:12Z

I think not. The current definition isn't used much and my proposed generalization is quite light.
By wrapper, I assume you mean a new definition?

src/data/set/pairwise.lean

eric-wieser · 2021-10-25T13:14:05Z

Note however that some lemmas do require the generalization I'm providing here, finset.prod_bUnion for example.

That's not included in this PR though, right?

src/data/set/pairwise.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/big_operators/basic.lean

eric-wieser · 2021-10-29T14:12:55Z

src/algebra/big_operators/basic.lean

@@ -303,20 +304,17 @@ end

 @[to_additive]
 lemma prod_bUnion [decidable_eq α] {s : finset γ} {t : γ → finset α} :
-  (∀ x ∈ s, ∀ y ∈ s, x ≠ y → disjoint (t x) (t y)) →
+  (set.pairwise_disjoint ↑s t) →


This feels like a slightly worse lemma than the original, as now the caller has to deal with awkward coercions.

It really is fine. After all, I managed to golf the proofs that were using it already.

# Conflicts: # src/data/set/pairwise.lean # src/measure_theory/covering/besicovitch.lean # src/measure_theory/covering/vitali.lean # src/topology/bases.lean

jcommelin

Thanks 🎉

bors merge

…se_disjoint` (#9898) This will allow to express the bind operation: you can't currently express that the pairwise disjoint union of pairwise disjoint sets pairwise disjoint. Here's the corresponding statement with `finset.sup_indep` (defined in #9867): ```lean lemma sup_indep.sup {s : finset ι'} {g : ι' → finset ι} {f : ι → α} (hs : s.sup_indep (λ i, (g i).sup f)) (hg : ∀ i' ∈ s, (g i').sup_indep f) : (s.sup g).sup_indep f := ``` You currently can't do `set.pairwise_disjoint s (λ i, ⋃ x ∈ g i, f x)`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

bors · 2021-11-04T15:29:21Z

Build failed (retrying...):

Build mathlib

…se_disjoint` (#9898) This will allow to express the bind operation: you can't currently express that the pairwise disjoint union of pairwise disjoint sets pairwise disjoint. Here's the corresponding statement with `finset.sup_indep` (defined in #9867): ```lean lemma sup_indep.sup {s : finset ι'} {g : ι' → finset ι} {f : ι → α} (hs : s.sup_indep (λ i, (g i).sup f)) (hg : ∀ i' ∈ s, (g i').sup_indep f) : (s.sup g).sup_indep f := ``` You currently can't do `set.pairwise_disjoint s (λ i, ⋃ x ∈ g i, f x)`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

bors · 2021-11-04T18:48:45Z

Pull request successfully merged into master.

Build succeeded:

…se_disjoint` (#9898) This will allow to express the bind operation: you can't currently express that the pairwise disjoint union of pairwise disjoint sets pairwise disjoint. Here's the corresponding statement with `finset.sup_indep` (defined in #9867): ```lean lemma sup_indep.sup {s : finset ι'} {g : ι' → finset ι} {f : ι → α} (hs : s.sup_indep (λ i, (g i).sup f)) (hg : ∀ i' ∈ s, (g i').sup_indep f) : (s.sup g).sup_indep f := ``` You currently can't do `set.pairwise_disjoint s (λ i, ⋃ x ∈ g i, f x)`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

YaelDillies added 4 commits October 22, 2021 16:26

initial commit

e0b12d2

fix

96556c4

fix support

53e0497

fix cycles

e03c85f

eric-wieser reviewed Oct 23, 2021

View reviewed changes

src/data/set/pairwise.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Oct 23, 2021

View reviewed changes

src/data/set/pairwise.lean Show resolved Hide resolved

YaelDillies added the awaiting-review The author would like community review of the PR label Oct 23, 2021

eric-wieser mentioned this pull request Oct 25, 2021

[Merged by Bors] - feat(order/partition/finpartition): Finite partitions #9795

Closed

2 tasks

eric-wieser reviewed Oct 25, 2021

View reviewed changes

src/data/set/pairwise.lean Show resolved Hide resolved

YaelDillies added 3 commits October 26, 2021 15:45

update docstrings, change prod_bUnion

d064429

fix ring

b5f34e8

fix cyclotomic

ae5e836

eric-wieser mentioned this pull request Oct 28, 2021

[Merged by Bors] - feat(order/sup_indep): Finite supremum independence #9867

Closed

eric-wieser reviewed Oct 28, 2021

View reviewed changes

src/data/set/pairwise.lean Outdated Show resolved Hide resolved

kill double space

3a754c2

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 28, 2021

Merge remote-tracking branch 'origin/master' into pw_disj_index

247d3b5

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 29, 2021

eric-wieser reviewed Oct 29, 2021

View reviewed changes

src/algebra/big_operators/basic.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Oct 29, 2021

View reviewed changes

eric-wieser mentioned this pull request Oct 29, 2021

[Merged by Bors] - chore(data/set/pairwise): rename set.pairwise_on to set.pairwise to match list.pairwise and multiset.pairwise #10035

Closed

YaelDillies added 4 commits October 29, 2021 18:13

replace s.pairwise_on (disjoint on f) by s.pairwise_disjoint f

a812475

fix

6be0cca

fix topology.bases

21b7cc4

fix measure_space

edc80af

YaelDillies added 3 commits October 29, 2021 22:36

fix vitali

4ccc9e8

fix universes and besicovitch

2252e44

add inj_on.pairwise_disjoint_image

84cca77

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 31, 2021

Merge remote-tracking branch 'origin/master' into pw_disj_index

0d5d8f7

# Conflicts: # src/data/set/pairwise.lean # src/measure_theory/covering/besicovitch.lean # src/measure_theory/covering/vitali.lean # src/topology/bases.lean

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 31, 2021

jcommelin approved these changes Nov 4, 2021

View reviewed changes

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Nov 4, 2021

bors bot changed the title ~~refactor(data/set/pairwise): Indexed sets as arguments to set.pairwise_disjoint~~ [Merged by Bors] - refactor(data/set/pairwise): Indexed sets as arguments to set.pairwise_disjoint Nov 4, 2021

bors bot closed this Nov 4, 2021

bors bot deleted the pw_disj_index branch November 4, 2021 18:48

YaelDillies mentioned this pull request Mar 21, 2022

[Merged by Bors] - feat(order/sup_indep): lemmas about pairwise and set.pairwise #12590

Closed

1 task

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(data/set/pairwise): Indexed sets as arguments to `set.pairwise_disjoint` #9898

[Merged by Bors] - refactor(data/set/pairwise): Indexed sets as arguments to `set.pairwise_disjoint` #9898

YaelDillies commented Oct 23, 2021 •

edited by eric-wieser

Loading

eric-wieser commented Oct 23, 2021

YaelDillies commented Oct 23, 2021

jcommelin commented Oct 25, 2021

YaelDillies commented Oct 25, 2021 •

edited

Loading

eric-wieser commented Oct 25, 2021

eric-wieser Oct 29, 2021

YaelDillies Oct 29, 2021

jcommelin left a comment

bors bot commented Nov 4, 2021

bors bot commented Nov 4, 2021

[Merged by Bors] - refactor(data/set/pairwise): Indexed sets as arguments to set.pairwise_disjoint #9898

[Merged by Bors] - refactor(data/set/pairwise): Indexed sets as arguments to set.pairwise_disjoint #9898

Conversation

YaelDillies commented Oct 23, 2021 • edited by eric-wieser Loading

eric-wieser commented Oct 23, 2021

YaelDillies commented Oct 23, 2021

jcommelin commented Oct 25, 2021

YaelDillies commented Oct 25, 2021 • edited Loading

eric-wieser commented Oct 25, 2021

eric-wieser Oct 29, 2021

Choose a reason for hiding this comment

YaelDillies Oct 29, 2021

Choose a reason for hiding this comment

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Nov 4, 2021

bors bot commented Nov 4, 2021

[Merged by Bors] - refactor(data/set/pairwise): Indexed sets as arguments to `set.pairwise_disjoint` #9898

[Merged by Bors] - refactor(data/set/pairwise): Indexed sets as arguments to `set.pairwise_disjoint` #9898

YaelDillies commented Oct 23, 2021 •

edited by eric-wieser

Loading

YaelDillies commented Oct 25, 2021 •

edited

Loading