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] - chore(Topology/Inseparable): re-use some variables #9808

Closed
wants to merge 23 commits into from
Closed

[Merged by Bors] - chore(Topology/Inseparable): re-use some variables #9808

wants to merge 23 commits into from

Conversation

grunweg
Copy link
Collaborator

@grunweg grunweg commented Jan 17, 2024

Found this when cleaning up old branches; here you are.

Open in Gitpod

grunweg and others added 23 commits December 25, 2023 17:36
@grunweg
Part 1, until line 460 (open maps).
cd0fdd7 
Create missing sections for new definitions.
Consolidate TopologicalSpace assumptions; re-use variable {f}.
@grunweg
Continue.
61281a6
@grunweg
Remainder.
c4a0ddc
@grunweg
Merge branch 'master' into MR-topology_maps-reusevars
4daef96
@grunweg
Fix build.
d2d8320
@grunweg
Review comments.
da91fc1
@grunweg
Add and use Inducing namespace.
c84410b
@grunweg
Collect variable {f : \alpha\to\beta} and {g:\beta\to\gamma}.
fe6f950
@grunweg
Re-use more variables; reflow some lines accordingly.
7d8888f
@grunweg
Gather {\iota: Type*} as well.
c6a82c7
@grunweg
Remove \delta variable; it's unused.
41dcbf4
@grunweg
Fix build.
e8d8185
@grunweg
Rename \alpha to X, \beta to Y and \gamma to Z.
faa18d5 
Using the new rename handler, hence should build everywhere...
@grunweg
A few manual fixups.
eef50e5
@grunweg
Re-use variables X and Y once.
0028c87
@grunweg
Rename one embedding from e to f; re-use function f once.
42232c7
@grunweg
Rename a : X to x; also for a_1 and a_2.
897e54f
@grunweg
Rename b : Y to y.
bd057c1
@grunweg
Rename b : X to x.
686d9ff
@grunweg
Rename _a and _b also.
5134206
@grunweg
Fix build.
59be689
@grunweg
Re-use a few {f : X \to Y} and {x : X} variables.
d0f7889
@grunweg
Merge branch 'master' into MR-topology-inseparable-reuse-vars
b95f8e6
@grunweg grunweg added awaiting-review The author would like community review of the PR easy < 20s of review time. See the lifecycle page for guidelines. t-topology Topological spaces, uniform spaces, metric spaces, filters labels Jan 17, 2024
@ADedecker
Copy link
Member

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Jan 17, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jan 17, 2024
@grunweg
chore(Topology/Inseparable): re-use some variables (#9808)
1dfae4b 
Co-authored-by: grunweg <grunweg@posteo.de>
@mathlib-bors
Copy link

mathlib-bors bot commented Jan 17, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Topology/Inseparable): re-use some variables [Merged by Bors] - chore(Topology/Inseparable): re-use some variables Jan 17, 2024
@mathlib-bors mathlib-bors bot closed this Jan 17, 2024
@mathlib-bors mathlib-bors bot deleted the MR-topology-inseparable-reuse-vars branch January 17, 2024 19:16
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
easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors. 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.

None yet
2 participants
@grunweg @ADedecker