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

Closed ball #283

Merged

CohenCyril merged 3 commits into master from closed_ball

Jan 15, 2021

Collaborator

mkerjean commented Nov 16, 2020

A theory of closed balls.

mkerjean force-pushed the closed_ball branch from e7f59be to 95ed722 Compare

November 16, 2020 20:04

Member

affeldt-aist commented Dec 4, 2020

note that PR #268 has been merged so that you can get rid of a few lemmas about closure after rebasing

mkerjean force-pushed the closed_ball branch 3 times, most recently from be41a50 to ec382ff Compare

December 8, 2020 17:07

CohenCyril reviewed

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

CohenCyril reviewed

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

CohenCyril reviewed

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

CohenCyril reviewed

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

CohenCyril reviewed

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

CohenCyril reviewed

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

mkerjean force-pushed the closed_ball branch 2 times, most recently from 9dba2f4 to f09c592 Compare

December 8, 2020 20:52

CohenCyril reviewed

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

CohenCyril reviewed

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

mkerjean force-pushed the closed_ball branch from 9f95ae2 to edd089f Compare

December 8, 2020 22:03

mkerjean commented

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

affeldt-aist mentioned this pull request

ax5 added to PseudoMetric.mixin_of #305

Closed

mkerjean commented

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

mkerjean force-pushed the closed_ball branch from 2b110bf to 0281aa3 Compare

January 14, 2021 21:13


          closed_ball

9cab8c9

Co-Auhored-By: Théo Vignon

Co-Authored-By: Cyril Cohen <CohenCyril@users.noreply.github.com>

Co-Authored-By: Reynald Affeldt @affeldt-aist

Co-Authored-By: @pi8027

mkerjean force-pushed the closed_ball branch from 0281aa3 to 9cab8c9 Compare

January 14, 2021 21:14

Collaborator Author

mkerjean commented Jan 14, 2021

I addressed all your comments @CohenCyril. It could be ready to be merged - or maybe another look at the proofs is necessary.


          proof-reading

90f2baf

- add changelog
- closed_neigh_ball' and closed_neigh_ball were the same lemmas so I removed the longer one
- minor proof compression and nitpicking
- rename closed_ball_int to interior_closed_ballE
  + because the _int suffix is maybe unclear
- move a piece of documentation in the header

Member

affeldt-aist commented Jan 15, 2021

(TBA topology.v) means to be added to topology.v?
- of course this can't be done right away because the lemmas here depend on ball_normE
- I observe that nbhs0_lt and nbhs'0_lt could be specialized to V = K^o
naming suggestions:
- closed_neigh_ball -> open_nbhs_closed_ball? (because we don't use the string "neigh")
- sub_closed_ball -> closed_ball_subset? (I think that the full string "subset" is privileged)
- ball_closed_ball -> subset_closed_ball? (might be easier to guess what the lemma provides)

affeldt-aist force-pushed the closed_ball branch from fc6baa0 to 90f2baf Compare

January 15, 2021 08:34

CohenCyril requested changes

View reviewed changes

Member

CohenCyril left a comment

Please update the changelog with the last renamings.
Aside from that we're good to go.


          renaming

b97664f

mkerjean force-pushed the closed_ball branch from 1ba0491 to b97664f Compare

January 15, 2021 16:20

CohenCyril approved these changes

View reviewed changes

Member

CohenCyril left a comment

LGTM

CohenCyril merged commit badb1d1 into master

affeldt-aist deleted the closed_ball branch

January 19, 2021 09:00

mkerjean mentioned this pull request

Balls should be provably open #301

Closed

affeldt-aist mentioned this pull request

Bounded and landau notations #271

Open

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet