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

feat(data/set/intervals): define intervals and prove basic properties #1949

Merged
merged 9 commits into from Feb 4, 2020
Merged

feat(data/set/intervals): define intervals and prove basic properties #1949

merged 9 commits into from Feb 4, 2020

Conversation

aceg00
Copy link
Collaborator

@aceg00 aceg00 commented Feb 4, 2020 •
edited

And some other things. Split from #1944. Same set of changes is made there. Using Icc (min a b) (max a b) does make thing a lot easier. Thanks! @urkud

TO CONTRIBUTORS:

Make sure you have:

  • reviewed and applied the coding style: coding, naming
  • reviewed and applied the documentation requirements
  • for tactics:
  • make sure definitions and lemmas are put in the right files
  • make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

@aceg00 aceg00 assigned urkud and unassigned digama0 Feb 4, 2020
@aceg00 aceg00 added the awaiting-review The author would like community review of the PR label Feb 4, 2020
sgouezel
sgouezel reviewed Feb 4, 2020
View reviewed changes
src/data/set/intervals/interval.lean Outdated Show resolved Hide resolved
src/data/set/intervals/interval.lean Outdated Show resolved Hide resolved
src/data/set/intervals/interval.lean Outdated Show resolved Hide resolved
src/data/set/intervals/interval.lean Outdated Show resolved Hide resolved
@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 Feb 4, 2020
@aceg00 aceg00 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 Feb 4, 2020
@urkud urkud 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 Feb 4, 2020
@mergify mergify bot merged commit 253f75c into leanprover-community:master Feb 4, 2020
jcommelin pushed a commit that referenced this pull request Feb 5, 2020
@urkud @mergify @jcommelin
feat(data/set/intervals): define intervals and prove basic properties (…
c3924bc 
…#1949)

* things about intervals

* better documentation

* better file name

* add segment_eq_interval

* better proof for is_measurable_interval

* better import and better proof

* better proof

Co-authored-by: Yury G. Kudryashov <urkud@ya.ru>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
mergify bot added a commit that referenced this pull request Feb 7, 2020
@jcommelin @sgouezel
@urkud @mergify @fpvandoorn @robertylewis @ChrisHughes24
feat(algebraic_geometry/prime_spectrum): first definitions (#1957)
f912a6b 
* Start on prime spectrum

* Define comap betwee prime spectra; prove continuity

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* chore(*): rename `filter.inhabited_of_mem_sets` to `nonempty_of_mem_sets` (#1943)

In other names `inhabited` means that we have a `default` element.

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* refactor(linear_algebra/multilinear): cleanup of multilinear maps (#1921)

* staging [ci skip]

* staging

* staging

* cleanup norms

* complete currying

* docstrings

* docstrings

* cleanup

* nonterminal simp

* golf

* missing bits for derivatives

* sub_apply

* cleanup

* better docstrings

* remove two files

* reviewer's comments

* use fintype

* line too long

Co-authored-by: Yury G. Kudryashov <urkud@ya.ru>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(ring_theory/power_series): several simp lemmas (#1945)

* Small start on generating functions

* Playing with Bernoulli

* Finished sum_bernoulli

* Some updates after PRs

* Analogue for mv_power_series

* Cleanup after merged PRs

* feat(ring_theory/power_series): several simp lemmas

* Remove file that shouldn't be there yet

* Update src/ring_theory/power_series.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Generalise lemma to canonically_ordered_monoid

* Update name

* Fix build

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(tactic/lint): Three new linters, update illegal_constants (#1947)

* add three new linters

* fix failing declarations

* restrict and rename illegal_constants linter

* update doc

* update ge_or_gt test

* update mk_nolint

* fix error

* Update scripts/mk_nolint.lean

Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>

* Update src/meta/expr.lean

Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>

* clarify unfolds_to_class

* fix names since name is no longer protected

also change one declaration back to instance, since it did not cause a linter failure

* fix errors, move notes to docstrings

* add comments to docstring

* update mk_all.sh

* fix linter errors

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(number_theory/bernoulli): Add definition of Bernoulli numbers (#1952)

* Small start on generating functions

* Playing with Bernoulli

* Finished sum_bernoulli

* Some updates after PRs

* Analogue for mv_power_series

* Cleanup after merged PRs

* feat(number_theory/bernoulli): Add definition of Bernoulli numbers

* Remove old file

* Process comments

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(topology/algebra/multilinear): define continuous multilinear maps (#1948)

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(data/set/intervals): define intervals and prove basic properties (#1949)

* things about intervals

* better documentation

* better file name

* add segment_eq_interval

* better proof for is_measurable_interval

* better import and better proof

* better proof

Co-authored-by: Yury G. Kudryashov <urkud@ya.ru>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* refactor(*): migrate from `≠ ∅` to `set.nonempty` (#1954)

* refactor(*): migrate from `≠ ∅` to `set.nonempty`

Sorry for a huge PR but it's easier to do it in one go.
Basically, I got rid of all `≠ ∅` in theorem/def types, then fixed
compile.

I also removed most lemmas about `≠ ∅` from `set/basic` to make sure
that I didn't miss something I should change elsewhere. Should I
restore (some of) them?

* Fix compile of `archive/`

* Drop +1 unneeded argument, thanks @sgouezel.

* Fix build

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Change I to s, and little fixes

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Indentation

* Update prime_spectrum.lean

* fix build

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Yury G. Kudryashov <urkud@ya.ru>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: Zhouhang Zhou <zhouhanz@andrew.cmu.edu>
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 15, 2020
@urkud @mergify @anrddh
feat(data/set/intervals): define intervals and prove basic properties (…
4103def 
…leanprover-community#1949)

* things about intervals

* better documentation

* better file name

* add segment_eq_interval

* better proof for is_measurable_interval

* better import and better proof

* better proof

Co-authored-by: Yury G. Kudryashov <urkud@ya.ru>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 15, 2020
@jcommelin @sgouezel
@urkud @mergify @fpvandoorn @robertylewis @ChrisHughes24 @anrddh
feat(algebraic_geometry/prime_spectrum): first definitions (leanprove…
aaed5e2 
…r-community#1957)

* Start on prime spectrum

* Define comap betwee prime spectra; prove continuity

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* chore(*): rename `filter.inhabited_of_mem_sets` to `nonempty_of_mem_sets` (leanprover-community#1943)

In other names `inhabited` means that we have a `default` element.

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* refactor(linear_algebra/multilinear): cleanup of multilinear maps (leanprover-community#1921)

* staging [ci skip]

* staging

* staging

* cleanup norms

* complete currying

* docstrings

* docstrings

* cleanup

* nonterminal simp

* golf

* missing bits for derivatives

* sub_apply

* cleanup

* better docstrings

* remove two files

* reviewer's comments

* use fintype

* line too long

Co-authored-by: Yury G. Kudryashov <urkud@ya.ru>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(ring_theory/power_series): several simp lemmas (leanprover-community#1945)

* Small start on generating functions

* Playing with Bernoulli

* Finished sum_bernoulli

* Some updates after PRs

* Analogue for mv_power_series

* Cleanup after merged PRs

* feat(ring_theory/power_series): several simp lemmas

* Remove file that shouldn't be there yet

* Update src/ring_theory/power_series.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Generalise lemma to canonically_ordered_monoid

* Update name

* Fix build

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(tactic/lint): Three new linters, update illegal_constants (leanprover-community#1947)

* add three new linters

* fix failing declarations

* restrict and rename illegal_constants linter

* update doc

* update ge_or_gt test

* update mk_nolint

* fix error

* Update scripts/mk_nolint.lean

Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>

* Update src/meta/expr.lean

Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>

* clarify unfolds_to_class

* fix names since name is no longer protected

also change one declaration back to instance, since it did not cause a linter failure

* fix errors, move notes to docstrings

* add comments to docstring

* update mk_all.sh

* fix linter errors

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(number_theory/bernoulli): Add definition of Bernoulli numbers (leanprover-community#1952)

* Small start on generating functions

* Playing with Bernoulli

* Finished sum_bernoulli

* Some updates after PRs

* Analogue for mv_power_series

* Cleanup after merged PRs

* feat(number_theory/bernoulli): Add definition of Bernoulli numbers

* Remove old file

* Process comments

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(topology/algebra/multilinear): define continuous multilinear maps (leanprover-community#1948)

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(data/set/intervals): define intervals and prove basic properties (leanprover-community#1949)

* things about intervals

* better documentation

* better file name

* add segment_eq_interval

* better proof for is_measurable_interval

* better import and better proof

* better proof

Co-authored-by: Yury G. Kudryashov <urkud@ya.ru>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* refactor(*): migrate from `≠ ∅` to `set.nonempty` (leanprover-community#1954)

* refactor(*): migrate from `≠ ∅` to `set.nonempty`

Sorry for a huge PR but it's easier to do it in one go.
Basically, I got rid of all `≠ ∅` in theorem/def types, then fixed
compile.

I also removed most lemmas about `≠ ∅` from `set/basic` to make sure
that I didn't miss something I should change elsewhere. Should I
restore (some of) them?

* Fix compile of `archive/`

* Drop +1 unneeded argument, thanks @sgouezel.

* Fix build

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Change I to s, and little fixes

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Indentation

* Update prime_spectrum.lean

* fix build

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Yury G. Kudryashov <urkud@ya.ru>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: Zhouhang Zhou <zhouhanz@andrew.cmu.edu>
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 16, 2020
@urkud @mergify @anrddh
feat(data/set/intervals): define intervals and prove basic properties (…
013ea79 
…leanprover-community#1949)

* things about intervals

* better documentation

* better file name

* add segment_eq_interval

* better proof for is_measurable_interval

* better import and better proof

* better proof

Co-authored-by: Yury G. Kudryashov <urkud@ya.ru>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 16, 2020
@jcommelin @sgouezel
@urkud @mergify @fpvandoorn @robertylewis @ChrisHughes24 @anrddh
feat(algebraic_geometry/prime_spectrum): first definitions (leanprove…
1d7a29d 
…r-community#1957)

* Start on prime spectrum

* Define comap betwee prime spectra; prove continuity

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* chore(*): rename `filter.inhabited_of_mem_sets` to `nonempty_of_mem_sets` (leanprover-community#1943)

In other names `inhabited` means that we have a `default` element.

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* refactor(linear_algebra/multilinear): cleanup of multilinear maps (leanprover-community#1921)

* staging [ci skip]

* staging

* staging

* cleanup norms

* complete currying

* docstrings

* docstrings

* cleanup

* nonterminal simp

* golf

* missing bits for derivatives

* sub_apply

* cleanup

* better docstrings

* remove two files

* reviewer's comments

* use fintype

* line too long

Co-authored-by: Yury G. Kudryashov <urkud@ya.ru>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(ring_theory/power_series): several simp lemmas (leanprover-community#1945)

* Small start on generating functions

* Playing with Bernoulli

* Finished sum_bernoulli

* Some updates after PRs

* Analogue for mv_power_series

* Cleanup after merged PRs

* feat(ring_theory/power_series): several simp lemmas

* Remove file that shouldn't be there yet

* Update src/ring_theory/power_series.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Generalise lemma to canonically_ordered_monoid

* Update name

* Fix build

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(tactic/lint): Three new linters, update illegal_constants (leanprover-community#1947)

* add three new linters

* fix failing declarations

* restrict and rename illegal_constants linter

* update doc

* update ge_or_gt test

* update mk_nolint

* fix error

* Update scripts/mk_nolint.lean

Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>

* Update src/meta/expr.lean

Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>

* clarify unfolds_to_class

* fix names since name is no longer protected

also change one declaration back to instance, since it did not cause a linter failure

* fix errors, move notes to docstrings

* add comments to docstring

* update mk_all.sh

* fix linter errors

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(number_theory/bernoulli): Add definition of Bernoulli numbers (leanprover-community#1952)

* Small start on generating functions

* Playing with Bernoulli

* Finished sum_bernoulli

* Some updates after PRs

* Analogue for mv_power_series

* Cleanup after merged PRs

* feat(number_theory/bernoulli): Add definition of Bernoulli numbers

* Remove old file

* Process comments

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(topology/algebra/multilinear): define continuous multilinear maps (leanprover-community#1948)

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* feat(data/set/intervals): define intervals and prove basic properties (leanprover-community#1949)

* things about intervals

* better documentation

* better file name

* add segment_eq_interval

* better proof for is_measurable_interval

* better import and better proof

* better proof

Co-authored-by: Yury G. Kudryashov <urkud@ya.ru>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

* refactor(*): migrate from `≠ ∅` to `set.nonempty` (leanprover-community#1954)

* refactor(*): migrate from `≠ ∅` to `set.nonempty`

Sorry for a huge PR but it's easier to do it in one go.
Basically, I got rid of all `≠ ∅` in theorem/def types, then fixed
compile.

I also removed most lemmas about `≠ ∅` from `set/basic` to make sure
that I didn't miss something I should change elsewhere. Should I
restore (some of) them?

* Fix compile of `archive/`

* Drop +1 unneeded argument, thanks @sgouezel.

* Fix build

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Change I to s, and little fixes

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/algebraic_geometry/prime_spectrum.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Indentation

* Update prime_spectrum.lean

* fix build

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Yury G. Kudryashov <urkud@ya.ru>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: Zhouhang Zhou <zhouhanz@andrew.cmu.edu>
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sgouezel sgouezel sgouezel left review comments

@urkud urkud urkud approved these changes

Assignees

@urkud urkud

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
4 participants
@aceg00 @urkud @sgouezel @digama0