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: generalize CompleteSpace (ContinuousMultilinearMap _ _ _) to TVS #13468

Closed
wants to merge 28 commits into from
Closed

[Merged by Bors] - feat: generalize CompleteSpace (ContinuousMultilinearMap _ _ _) to TVS #13468

wants to merge 28 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Jun 2, 2024 •
edited by sgouezel
Loading

urkud added 19 commits February 24, 2024 22:05
@urkud
Snapshot
83efc0a
@urkud
Snapshot
5c90625
@urkud
chore(Topology/Sequences): split file
535c349 
I want to have access to the definitions much earlier.
Also, most of the file doesn't need metric spaces at all.
@urkud
Merge branch 'YK-seq-split' into YK-topgenfam
1bc1e88
@urkud
Snapshot
6c419e3
@urkud
feat(UniformSpace/Cauchy): add lemmas about TotallyBounded
c675493
@urkud
Merge master into YK-topgenfam (using imerge)
2b1bd07
@urkud
Update
a52b4a2
@urkud
Update Mathlib/Topology/Defs/Induced.lean
0fdfcfa
@urkud
Add docs, use for isClosed_setOf_continuous
7fd2b50
@urkud
Merge branch 'master' into YK-completeSpace
f527579
@urkud
Update
a1fc50b
@urkud
Merge branch 'master' into YK-completeSpace
d34d1eb
@urkud
Merge branch 'YK-totbdd' into YK-completeSpace
d9316ba
@urkud
Update
e4953f1
@urkud
Revert irrelevant changes
777a394
@urkud
Merge branch 'master' into YK-topgenfam
9dbccc6
@urkud
Update
c169b69
@urkud
Revert more
9a06bed
@urkud urkud added t-topology Topological spaces, uniform spaces, metric spaces, filters t-analysis Analysis (normed *, calculus) blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) awaiting-review labels Jun 2, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels Jun 29, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Jun 30, 2024 •
edited
Loading

PR summary 2bf2e223c5

Import changes

No significant changes to the import graph

Declarations diff

+ Filter.Tendsto.isVonNBounded_range
+ instCompleteSpace
+ range_toUniformOnFun
+ uniformContinuous_eval

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 30, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels Jun 30, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 1, 2024
@urkud urkud removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 1, 2024
@sgouezel
Copy link
Contributor

sgouezel commented Jul 1, 2024

bors r+
Thanks!

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 1, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 1, 2024
@urkud
feat: generalize CompleteSpace (ContinuousMultilinearMap _ _ _) to …
050f5a8 
…TVS (#13468)
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 1, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: generalize CompleteSpace (ContinuousMultilinearMap _ _ _) to TVS [Merged by Bors] - feat: generalize CompleteSpace (ContinuousMultilinearMap _ _ _) to TVS Jul 1, 2024
@mathlib-bors mathlib-bors bot closed this Jul 1, 2024
@mathlib-bors mathlib-bors bot deleted the YK-completeSpace branch July 1, 2024 14:30
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@urkud @dagurtomas
feat: generalize CompleteSpace (ContinuousMultilinearMap _ _ _) to …
7e9dade 
…TVS (#13468)
@adomani adomani mentioned this pull request Aug 1, 2024
Open
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
ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus) t-topology Topological spaces, uniform spaces, metric spaces, filters
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@urkud @leanprover-community-mathlib4-bot @sgouezel