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/finset/intervals, data/set/intervals/basic): intersection of finset.Ico, union of intervals for sets and finsets #5410

Closed
wants to merge 17 commits into from
Closed

[Merged by Bors] - feat(data/finset/intervals, data/set/intervals/basic): intersection of finset.Ico, union of intervals for sets and finsets #5410

wants to merge 17 commits into from

Conversation

RemyDegenne
Copy link
Collaborator

@RemyDegenne RemyDegenne added the awaiting-review The author would like community review of the PR label Dec 17, 2020
sgouezel
sgouezel reviewed Dec 19, 2020
View reviewed changes
Copy link
Collaborator

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

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

Can't these lemmas be deduced from the same statements for usual Ico's, over a general linear order? Having these lemmas also over reals or rationals would probably be useful in some situations.

@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Dec 19, 2020
@RemyDegenne
Copy link
Collaborator Author

I don't understand what you are suggesting.
All possible lemmas about intersection and union of Ico/Icc/... already exist for sets, in data.set.intervals.basic .
The only intervals I see for finset are these ones in data.finset.intervals, which are only Ico for N.

@RemyDegenne RemyDegenne added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Dec 19, 2020
@sgouezel
Copy link
Collaborator

If the lemmas you are looking for already exist for intervals, then you should be able to use them to prove your finset.Ico versions, to get very short proofs, no?

@RemyDegenne
Copy link
Collaborator Author

Ok, now I understand!
I think that I will need to first add some lemmas to link the set and finset worlds. For example to say that the coe of a finset.Ico is a set.Ico over N, which I don't see anywhere.

@RemyDegenne
Copy link
Collaborator Author

And I was wrong about the corresponding lemma for sets being already in mathlib (I misread the hypotheses of some other lemma). I'll do those as well.

@RemyDegenne RemyDegenne added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Dec 19, 2020
@RemyDegenne RemyDegenne added the WIP Work in progress label Dec 19, 2020
@RemyDegenne
Copy link
Collaborator Author

I added lemmas for union of set intervals of the form I**_union_I** (ex Ico_union_Ici) for (I think) all cases for which the shape of the resulting interval does not depend on additional hypotheses. Example: Ico_union_Ico is an Ico whenever it is an interval, but a lemma Ico_union_Ioc would need additional hypotheses to determine whether the results is Ioo, Icc or something else, hence the first one is included, but not the second one.

The lemmas are provided in two versions (with names Ico_union_Ico' and Ico_union_Ico), depending on the hypotheses. For Ioc (and only for Ioc), there was already a Ioc_union_Ioc result. I therefore used the name without a prime to denote the lemma that corresponds to the hypotheses of that result.

For finsets, I added simp and norm_cast attributes to the coe_eq_Ico lemma. I am unsure about what should have a norm_cast attribute, so I would like an input on that. I wrote two union results and an inter lemma.

@RemyDegenne RemyDegenne changed the title feat(data/finset/intervals): intersection of finset.Ico, union of overlapping finset.Ico feat(data/finset/intervals, data/set/intervals/basic): intersection of finset.Ico, union of intervals for sets and finsets Jan 3, 2021
@RemyDegenne RemyDegenne added awaiting-review The author would like community review of the PR and removed WIP Work in progress awaiting-author A reviewer has asked the author a question or requested changes labels Jan 3, 2021
@sgouezel
Copy link
Collaborator

sgouezel commented Jan 8, 2021

bors r+
Thanks!

@github-actions 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 Jan 8, 2021
bors bot pushed a commit that referenced this pull request Jan 8, 2021
@RemyDegenne
feat(data/finset/intervals, data/set/intervals/basic): intersection o…
aab5994 
…f finset.Ico, union of intervals for sets and finsets (#5410)
@bors
Copy link

bors bot commented Jan 9, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/finset/intervals, data/set/intervals/basic): intersection of finset.Ico, union of intervals for sets and finsets [Merged by Bors] - feat(data/finset/intervals, data/set/intervals/basic): intersection of finset.Ico, union of intervals for sets and finsets Jan 9, 2021
@bors bors bot closed this Jan 9, 2021
@bors bors bot deleted the ico_union_inter branch January 9, 2021 00:40
Julian added a commit that referenced this pull request Jan 12, 2021
@Julian
Merge remote-tracking branch 'origin/master' into freek-45
2be7703 
* origin/master: (751 commits)
  chore(topology/algebra/infinite_sum): speedup has_sum_sum (#5710)
  feat(submonoid/basic): subsingleton and nontrivial instances for {add_,}submonoid (#5690)
  docs(undergrad.yaml): analysis updates (#5675)
  feat(linear_algebra/multilinear_map): Add `range` and `map` (#5658)
  feat(measure_theory): each set has a measurable superset of the same measure (#5688)
  feat(data/set/intervals): add 2 Icc ssubset lemmas (#5617)
  chore(category_theory/limits): move constructions folder (#5681)
  fix(linear_algebra/tensor_product): Remove the priorities from the module structure (#5667)
  chore(category_theory/limits/over): generalise, golf and document over limits (#5674)
  chore(scripts): update nolints.txt (#5705)
  feat(measure_theory/pi): `ae_eq` lemmas about intervals in `Π i, α i` (#5633)
  feat(algebra/splitting_field): Restrict to splitting field (#5562)
  chore(scripts): update nolints.txt (#5699)
  feat(analysis/special/functions/trigonometric): complex trig and some even/odd lemmas (#5404)
  feat(equiv|set|topology): various additions (#5656)
  chore(measure_theory/set_integral): use weaker assumptions here and there (#5647)
  feat(field_theory/separable): Remove hypothesis in irreducible.separable (#5687)
  feat(order/complete_well_founded): characterise well-foundedness for complete lattices (#5575)
  chore(order/filter): a few more lemmas about `eventually` and set operations (#5686)
  chore(order/filter/basic): a few `simp` lemmas (#5685)
  feat(data/equiv/basic, logic/embedding): swap commutes with injective functions (#5636)
  chore(scripts): update nolints.txt (#5682)
  feat(algebra/lie/basic): Lie ideal operations are linear spans (#5676)
  feat(measure_theory/lp_space): add more lemmas about snorm (#5644)
  chore(data/set/lattice): add a few simp lemmas (#5671)
  feat(topology/separation, topology/metric_space/basic): add lemmas on discrete subsets of a topological space (#5523)
  feat(topology/algebra/ordered): prove `tendsto.Icc` for pi-types (#5639)
  chore(scripts): update nolints.txt (#5673)
  feat(category_theory/limits): preserving pullbacks (#5668)
  chore(linear_algebra/alternating): golf a proof (#5666)
  chore(algebra/group/hom): fix additive version of docstring (#5660)
  chore(analysis/special_functions/trigonometric): adding `@[pp_nodot]` to complex.log (#5670)
  feat(data/finset/intervals, data/set/intervals/basic): intersection of finset.Ico, union of intervals for sets and finsets (#5410)
  feat(algebra/linear_ordered_comm_group_with_zero): Add linear_ordered_comm_monoid_with_zero and an instance for nat (#5645)
  feat(geometry/manifold/times_cont_mdiff): API for checking `times_cont_mdiff` (#5631)
  feat(category_theory/closed): Frobenius reciprocity of cartesian closed categories (#5624)
  feat(measure_theory/measure_space): ae_measurable and measurable are equivalent for complete measures (#5643)
  refactor(linear_algebra/alternating): Use unapplied maps when possible (#5648)
  chore(algebra/ordered_monoid): rename lemmas (#5657)
  feat(measure_theory/borel_space): locally finite measure is sigma finite (#5634)
  refactor(algebra/module/basic): Clean up all the nat/int semimodule definitions (#5654)
  feat(topology/algebra): add additive/multiplicative instances (#5662)
  chore(scripts): update nolints.txt (#5661)
  feat(measure_theory): some additions (#5653)
  chore(data/list/basic): tag mmap(') with simp (#5443)
  feat(category_theory/sites): category of sheaves on the trivial topology  (#5651)
  feat(category_theory/monad): reflector preserves terminal object (#5649)
  feat(measure_theory/borel_space): a compact set has finite measure (#5628)
  feat(category_theory/closed): golf definition and proofs (#5623)
  feat(category_theory/limits): the product comparison natural transformation (#5621)
  ...
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@sgouezel sgouezel Awaiting requested review from sgouezel

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@RemyDegenne @sgouezel @eric-wieser