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.

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

LinearContinuousBounded #183

Merged
merged 7 commits into from
Feb 18, 2021
Merged

Conversation

mkerjean
Copy link
Collaborator

@mkerjean mkerjean commented Apr 14, 2020

Lemmas showing that for functions between normed vector spaces, boundedness and continuity are equivalent.

theories/normedtype.v Outdated Show resolved Hide resolved
theories/normedtype.v Outdated Show resolved Hide resolved
theories/normedtype.v Outdated Show resolved Hide resolved
theories/normedtype.v Outdated Show resolved Hide resolved
theories/normedtype.v Outdated Show resolved Hide resolved
theories/normedtype.v Outdated Show resolved Hide resolved
@affeldt-aist affeldt-aist force-pushed the mathcomp_master branch 12 times, most recently from 5cc9b78 to 0afbda8 Compare April 22, 2020 12:48
@affeldt-aist affeldt-aist force-pushed the mathcomp_master branch 2 times, most recently from 4d1cc32 to 4905f3c Compare April 22, 2020 21:09
@mkerjean mkerjean marked this pull request as draft April 23, 2020 13:51
@affeldt-aist affeldt-aist force-pushed the mathcomp_master_linearcontinuousbounded branch 2 times, most recently from dff125c to 2fcd3af Compare April 23, 2020 14:41
@affeldt-aist affeldt-aist changed the base branch from mathcomp_master to master April 24, 2020 21:21
@affeldt-aist affeldt-aist changed the base branch from master to mathcomp_master April 24, 2020 21:21
@CohenCyril
Copy link
Member

Should be reopened on top of master (please add a reference to this PR so that we can continue the discussions)

@affeldt-aist affeldt-aist force-pushed the mathcomp_master_linearcontinuousbounded branch from 454e4ab to d6e5b98 Compare April 28, 2020 14:36
@affeldt-aist affeldt-aist changed the base branch from mathcomp_master to master April 28, 2020 14:37
@affeldt-aist affeldt-aist force-pushed the mathcomp_master_linearcontinuousbounded branch from d6e5b98 to 559e0ee Compare May 4, 2020 16:29
@mkerjean mkerjean force-pushed the mathcomp_master_linearcontinuousbounded branch from 1dae0fc to 1426bd8 Compare October 12, 2020 08:56
@affeldt-aist affeldt-aist removed this from the 0.3.3 milestone Nov 5, 2020
This was referenced Nov 5, 2020
@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
theories/normedtype.v Outdated Show resolved Hide resolved
@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 marked this pull request as ready for review January 19, 2021 08:59
@affeldt-aist affeldt-aist force-pushed the mathcomp_master_linearcontinuousbounded branch from 9772c3b to bb72254 Compare January 27, 2021 02:49
@affeldt-aist
Copy link
Member

affeldt-aist commented Jan 27, 2021

(I just rebased to get rid of conflicts and fix the changelog so that we can merge.) @CohenCyril

@affeldt-aist affeldt-aist force-pushed the mathcomp_master_linearcontinuousbounded branch from e1781e7 to 26b6b11 Compare January 27, 2021 03:33
@affeldt-aist affeldt-aist force-pushed the mathcomp_master_linearcontinuousbounded branch from 26b6b11 to 975430c Compare January 27, 2021 08:24
@mkerjean
Copy link
Collaborator Author

Should this be merged ?

@mkerjean mkerjean mentioned this pull request Feb 18, 2021
Copy link
Member

@CohenCyril CohenCyril left a comment

Choose a reason for hiding this comment

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

Yes! looks good to me!

@CohenCyril CohenCyril merged commit 41bfaac into master Feb 18, 2021
@affeldt-aist affeldt-aist deleted the mathcomp_master_linearcontinuousbounded branch March 12, 2021 02:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants