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(counterexamples/seminorm_lattice_not_distrib): The lattice of seminorms is not distributive. #12099

Closed
wants to merge 21 commits into from
Closed

[Merged by Bors] - feat(counterexamples/seminorm_lattice_not_distrib): The lattice of seminorms is not distributive. #12099

wants to merge 21 commits into from

Conversation

pbazin
Copy link
Collaborator

@pbazin pbazin commented Feb 17, 2022 •
edited by eric-wieser

A counterexample showing the lattice of seminorms is not distributive

Open in Gitpod

pbazin and others added 13 commits February 3, 2022 10:15
@pbazin
Adding the definition of the infimum of seminorms,
e1426fd 
and proving it behaves as an infimum.
@pbazin
Adding the definion of the infimum of seminorms,
d77c2a2 
and proving it behaves as an infimum.
@kbuzzard
remove noise
5804851
@pbazin
Adding brackets to separate different goals
0d36496
@pbazin
Indenting properly and simplifying parts of the proofs.
3439a9a
@pbazin
Added lemma le_insert for seminorms
2f80815
@pbazin
Made some arguments implicit
ef10db3
@pbazin
Moved definition of inf outside of seminorm ball section
6359746 
+ other small changes
@pbazin @mcdoll
Update src/analysis/seminorm.lean
9139f2c 
Co-authored-by: mcdoll <moritz.doll@googlemail.com>
@pbazin
format
71ec952
@pbazin
Merge branch 'seminorm_inf' of https://github.com/leanprover-communit…
3fbb25a 
…y/mathlib into seminorm_inf
@PatrickMassot
Add missing lemma
13b46e5
@pbazin
feat(counteramples/seminorm_lattice_not_distrib): The seminorm lattic…
604ab19 
…e is not distributive
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Feb 17, 2022
@pbazin pbazin mentioned this pull request Feb 17, 2022
Closed
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Feb 22, 2022
@leanprover-community-bot-assistant
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Feb 22, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Feb 22, 2022
@eric-wieser eric-wieser added the awaiting-author A reviewer has asked the author a question or requested changes label Feb 22, 2022
@pbazin pbazin 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 23, 2022
@eric-wieser eric-wieser 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 Mar 2, 2022
pbazin and others added 3 commits March 2, 2022 17:07
@pbazin @eric-wieser
fix comment orthograph
26685d9 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@pbazin @eric-wieser
fix indent
c24943e 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@pbazin @YaelDillies
fix comment
968584d 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@pbazin pbazin 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 Mar 2, 2022
eric-wieser
eric-wieser approved these changes Mar 2, 2022
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

LGTM! Perhaps someone else should take a final look before merging.

jcommelin
jcommelin approved these changes Mar 4, 2022
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 Mar 4, 2022
bors bot pushed a commit that referenced this pull request Mar 4, 2022
@pbazin @kbuzzard
@PatrickMassot @eric-wieser
feat(counterexamples/seminorm_lattice_not_distrib): The lattice of se…
09c66fa 
…minorms is not distributive. (#12099)

A counterexample showing the lattice of seminorms is not distributive



Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: pbazin <75327486+pbazin@users.noreply.github.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@bors
Copy link

bors bot commented Mar 4, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(counterexamples/seminorm_lattice_not_distrib): The lattice of seminorms is not distributive. [Merged by Bors] - feat(counterexamples/seminorm_lattice_not_distrib): The lattice of seminorms is not distributive. Mar 4, 2022
@bors bors bot closed this Mar 4, 2022
@bors bors bot deleted the seminorm_inf_counterexample branch March 4, 2022 10:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@YaelDillies YaelDillies YaelDillies left review comments

@eric-wieser eric-wieser eric-wieser approved these changes

@jcommelin jcommelin jcommelin approved these changes

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
7 participants
@pbazin @leanprover-community-bot-assistant @eric-wieser @jcommelin @YaelDillies @kbuzzard @PatrickMassot