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(Set): API for subset restriction and coercion to/from subtypes #9940

Closed

miguelmarco wants to merge 45 commits into master from subset

Collaborator

miguelmarco commented Jan 23, 2024 •

edited by kmill

Api for subset restriction and coercion to/from subtypes

Co-authored-by: Miguel Marco mmarco@unizar.es

miguelmarco and others added 6 commits

January 20, 2024 22:55


          First prototype of api for subste restrictions


          Implement coercion for sets

971becf


          Change to split operations

6a12b09


          Add arrow-up notation in the infoview

e08c6bc


          Fix linting issues

1975bf6


          Fix import and remove repeated simp lemmas

4ab3575

miguelmarco requested review from semorrison, kmill, eric-wieser, kbuzzard and winstonyin

January 23, 2024 21:30

miguelmarco added awaiting-review new-contributor labels

winstonyin reviewed

View reviewed changes

Mathlib/Data/Set/Subset.lean Outdated Show resolved Hide resolved

winstonyin reviewed

View reviewed changes

Mathlib/Data/Set/Subset.lean Outdated Show resolved Hide resolved

kmill reviewed

View reviewed changes

Contributor

kmill left a comment

I'll try to take a look later, but I just want to register my opinion that I think this notation is a neat idea.

Style note: I see a lot of places with an extra space character, like in x ∈ (↑D : Set α) for example. I wish we had an autoformatter for you, but you'll have to go through and find these.

winstonyin reviewed

View reviewed changes

Mathlib/Data/Set/Subset.lean Outdated Show resolved Hide resolved

winstonyin reviewed

View reviewed changes

Mathlib/Data/Set/Subset.lean Outdated Show resolved Hide resolved

winstonyin reviewed

View reviewed changes

Mathlib/Data/Set/Subset.lean Outdated Show resolved Hide resolved


          Merge remote-tracking branch 'origin/master' into subset

ae9d2eb

Collaborator

winstonyin commented Jan 25, 2024

I gave some minor style comments. There are also some inconsistent white spaces, which we can deal with at the end. I merged master into this so I can test it on my recent commit; hope you don't mind.

Collaborator

winstonyin commented Jan 25, 2024

Just tested it out. This is great and will make dealing with subtypes far less painful. For my use case, I need this API to also work with closure and continuity. I'd be happy to build on your work to make this happen if you don't plan on implementing these features.

winstonyin reviewed

View reviewed changes

Mathlib/Data/Set/Subset.lean Outdated Show resolved Hide resolved

eric-wieser reviewed

View reviewed changes

Mathlib/Data/Set/Subset.lean Outdated Show resolved Hide resolved

eric-wieser reviewed

View reviewed changes

Mathlib/Data/Set/Subset.lean Outdated Show resolved Hide resolved

miguelmarco added 5 commits

January 26, 2024 18:32


          address style changes from review

c70e7f1


          Merge branch 'subset' of github.com:leanprover-community/mathlib4 int…

84caaac

…o subset


          fix whitespaces

7164b8a


          define setRestrict as inverse image of coercion

719245c


          Fix linting

30d5bb6

miguelmarco added 5 commits

February 10, 2024 17:34


          yet another deduplication

6ec74cb


          Fix broken proof

b5e347e


          add preimage_val_sInter_eq_sInter

98a48d3


          oops

eb21b6a


          Add lemma about "going up and then down"

c6bf7a3

leanprover-community-mathlib4-bot added blocked-by-other-PR and removed blocked-by-other-PR labels

miguelmarco added 2 commits

February 19, 2024 21:25


          Merge remote-tracking branch 'origin/master' into subset

da816ed


          Adapt to merged #10433

9eca74e

miguelmarco added awaiting-review and removed awaiting-author labels

miguelmarco added 2 commits

February 20, 2024 00:23


          Remove redundant lemma

03dcb27


          Mark some lemmas as non-simp

69a2365

miguelmarco requested review from kmill and eric-wieser

February 20, 2024 14:54

Collaborator Author

miguelmarco commented Feb 22, 2024

Ping @kmill @eric-wieser

kmill reviewed

View reviewed changes

Mathlib/Data/Set/Image.lean Outdated Show resolved Hide resolved


          Update Mathlib/Data/Set/Image.lean

cb8d85b

Contributor

kmill commented Mar 3, 2024

Thanks! Creating a new notation for a new concept is a difficult first PR (or really any PR), but I think this is now in a good enough of a state to merge.

bors r+

github-actions bot added ready-to-merge and removed awaiting-review labels

mathlib-bors bot pushed a commit that referenced this pull request


          feat(Set): API for subset restriction and coercion to/from subtypes (#…

52762e2

…9940)

Api for subset restriction and coercion to/from subtypes

Co-authored-by: Miguel Marco <mmarco@unizar.es>



Co-authored-by: Miguel Marco <mmarco@unizar.es>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: mmarco <mmarco@kali>
Co-authored-by: Winston Yin <winstonyin@gmail.com>

mathlib-bors bot commented Mar 3, 2024

Pull request successfully merged into master.

Build succeeded:

mathlib-bors bot changed the title ~~feat(Set): API for subset restriction and coercion to/from subtypes~~ [Merged by Bors] - feat(Set): API for subset restriction and coercion to/from subtypes

mathlib-bors bot closed this

mathlib-bors bot deleted the subset branch

March 3, 2024 23:04

kbuzzard pushed a commit that referenced this pull request


          feat(Set): API for subset restriction and coercion to/from subtypes (#…

510ca4e

…9940)

Api for subset restriction and coercion to/from subtypes

Co-authored-by: Miguel Marco <mmarco@unizar.es>



Co-authored-by: Miguel Marco <mmarco@unizar.es>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: mmarco <mmarco@kali>
Co-authored-by: Winston Yin <winstonyin@gmail.com>

dagurtomas pushed a commit that referenced this pull request


          feat(Set): API for subset restriction and coercion to/from subtypes (#…

1d2f225

…9940)

Api for subset restriction and coercion to/from subtypes

Co-authored-by: Miguel Marco <mmarco@unizar.es>



Co-authored-by: Miguel Marco <mmarco@unizar.es>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: mmarco <mmarco@kali>
Co-authored-by: Winston Yin <winstonyin@gmail.com>

utensil pushed a commit that referenced this pull request


          feat(Set): API for subset restriction and coercion to/from subtypes (#…

4679b8f

…9940)

Api for subset restriction and coercion to/from subtypes

Co-authored-by: Miguel Marco <mmarco@unizar.es>



Co-authored-by: Miguel Marco <mmarco@unizar.es>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: mmarco <mmarco@kali>
Co-authored-by: Winston Yin <winstonyin@gmail.com>

Louddy pushed a commit that referenced this pull request


          feat(Set): API for subset restriction and coercion to/from subtypes (#…

d99aa32

…9940)

Api for subset restriction and coercion to/from subtypes

Co-authored-by: Miguel Marco <mmarco@unizar.es>



Co-authored-by: Miguel Marco <mmarco@unizar.es>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: mmarco <mmarco@kali>
Co-authored-by: Winston Yin <winstonyin@gmail.com>

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

Reviewers

kmill kmill left review comments

github-actions[bot] github-actions left review comments

kbuzzard Awaiting requested review from kbuzzard

winstonyin Awaiting requested review from winstonyin

eric-wieser Awaiting requested review from eric-wieser