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

Banach-Steinhaus #262

Closed
wants to merge 37 commits into from
Closed

Banach-Steinhaus #262

wants to merge 37 commits into from

Conversation

mkerjean
Copy link
Collaborator

Banach-Steinhaus Theorem, through Baire's Theorem.

This PR depends on PR#183 (linearcontinuousbounded)

@mkerjean mkerjean added the WIP label Sep 24, 2020
@mkerjean mkerjean changed the title init Banach-Steinhaus Sep 28, 2020
@mkerjean mkerjean force-pushed the mathcomp_master_linearcontinuousbounded branch 3 times, most recently from 1dae0fc to 1426bd8 Compare October 12, 2020 08:56
@affeldt-aist affeldt-aist marked this pull request as draft November 5, 2020 10:04
@affeldt-aist affeldt-aist removed the WIP label Nov 5, 2020
@affeldt-aist
Copy link
Member

Maybe this should now be rebased on top of PR #267 that subsumes PR #183 and is now under review.

@mkerjean mkerjean force-pushed the mathcomp_master_linearcontinuousbounded branch from 9bb50cb to d8fd180 Compare November 25, 2020 16:35
@mkerjean mkerjean force-pushed the mathcomp_master_linearcontinuousbounded branch 2 times, most recently from 9f39489 to bd50783 Compare January 14, 2021 22:01
@affeldt-aist affeldt-aist force-pushed the mathcomp_master_linearcontinuousbounded branch from 946ddb5 to c752404 Compare January 18, 2021 11:32
@affeldt-aist affeldt-aist force-pushed the mathcomp_master_linearcontinuousbounded branch 3 times, most recently from 26b6b11 to 975430c Compare January 27, 2021 08:24
@mkerjean mkerjean closed this Feb 18, 2021
@mkerjean mkerjean deleted the banach_steinhaus branch February 18, 2021 15:14
@CohenCyril
Copy link
Member

Hi. Did you reopen this PR elsewhere?

@mkerjean
Copy link
Collaborator Author

Hi. Did you reopen this PR elsewhere?

Yes, in the branch banachsteinhaus. The squashing of 37commits was too painful. I will PR the new branch once the rebasing on master is done, hopefully tonight.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@mkerjean @affeldt-aist @CohenCyril