Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

feat(combinatorics/simple_graph/ends): an infinite (preconnected, locally finite) graph has nonempty ends#18410

Closed
bottine wants to merge 64 commits intomasterfrom
bottine/simple_graph.ends/infinite
Closed

feat(combinatorics/simple_graph/ends): an infinite (preconnected, locally finite) graph has nonempty ends#18410
bottine wants to merge 64 commits intomasterfrom
bottine/simple_graph.ends/infinite

Conversation

@bottine
Copy link
Copy Markdown
Collaborator

@bottine bottine commented Feb 9, 2023 •
edited by YaelDillies
Loading

bottine and others added 30 commits December 8, 2022 11:44
@bottine
merge
2529a2c
@bottine
cleanup?
b7d462d
@bottine
inf_comp_out
812364d
@bottine @YaelDillies
Update src/combinatorics/simple_graph/ends/defs.lean
fb3f2f8 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@bottine
cosmetic
baecb96
@bottine
docstrings
0d1b4c3
@0art0
Expand subtype in out_hom and golf proofs
b751399
@0art0
Merge branch 'bottine/simple_graph/ends_for_real_this_time' of https:…
55ebf1f 
…//github.com/leanprover-community/mathlib into bottine/simple_graph/ends_for_real_this_time
@0art0
Erase diff artefact
7b09ed3
@bottine
finite graphs have no end
78ab79c
@bottine
docstring
69b305a
@bottine @YaelDillies
Apply suggestions from code review
8896528 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@bottine
errors
3dc91f1
@bottine
errors'
2f59b64
@bottine
op
9b8fca7
@bottine @YaelDillies
Update src/combinatorics/simple_graph/ends/properties.lean
74a79df 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@bottine
comp_out.hom reverse order and error
b2e5f0a
@bottine
better names
bc7b6ed
@bottine
Yael's suggestion
565868a
@bottine
forgot this
9f4c284
@bottine @YaelDillies
Apply suggestions from code review
72f2084 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@bottine @kmill
Kyle's suggestions
11f0d5b 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@0art0 @kmill
Update src/combinatorics/simple_graph/ends/defs.lean
1829b62 
Change spacing

Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@bottine
Kyle's suggestions
fbc6a77 
Co-authored-by: Kyle Miller <mill31415@gmail.com>
@bottine
a few lemmas + tweaks
bd19102
@bottine
some golf
372a409
@bottine
some of Yael's suggestions
8fcdc88
@bottine
better
9f61685
@bottine
tweaks
4f2d83f
@bottine
Yael's suggestions
155b3c7
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Mar 1, 2023
@ghost
Copy link
Copy Markdown

ghost commented Mar 1, 2023

This PR/issue depends on:

YaelDillies
YaelDillies reviewed Mar 1, 2023
View reviewed changes
YaelDillies
YaelDillies reviewed Mar 1, 2023
View reviewed changes
bottine and others added 2 commits March 1, 2023 15:47
@bottine @YaelDillies
Update src/combinatorics/simple_graph/ends/properties.lean
68c439e 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@bottine @YaelDillies
Update src/combinatorics/simple_graph/ends/properties.lean
847a7ce 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
YaelDillies
YaelDillies reviewed Mar 1, 2023
View reviewed changes
Copy link
Copy Markdown
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

This looks alright. Can you open a matching PR?

@bottine bottine mentioned this pull request Mar 1, 2023
Closed
@bottine
Copy link
Copy Markdown
Collaborator Author

bottine commented Mar 1, 2023 •
edited
Loading

This looks alright. Can you open a matching PR?

Opening an empty PR to be filled once things are merged in mathlib3 is fine? I tried creating a branch with no commit but the web UI doesn't allow creating a PR out of that.
By the way, would it make sense/be allowed to have a single mathlib4 PR for each of #18442 #18410 and #18454 ?

In any case, I'll wait for #18410 to get merged before moving further, to ensure no new conflict.

0art0 added a commit to bottine/mathlib that referenced this pull request Mar 1, 2023
@0art0
Incorporate changes from leanprover-community#18410
a493a21
0art0 added a commit to bottine/mathlib that referenced this pull request Mar 2, 2023
@0art0
Integrate changes from leanprover-community#18410
7eef3fd
@bottine
Copy link
Copy Markdown
Collaborator Author

bottine commented Mar 2, 2023

@YaelDillies I expect you've seen that comment; so I guess I won't open any mathlib4 PR, if that works for you too.

YaelDillies
YaelDillies approved these changes Mar 26, 2023
View reviewed changes
Copy link
Copy Markdown
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

maintainer merge. Thanks!

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 26, 2023

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@kim-em kim-em added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Mar 26, 2023
@bottine bottine mentioned this pull request Mar 28, 2023
Draft
4 tasks
@bottine
Copy link
Copy Markdown
Collaborator Author

bottine commented Mar 29, 2023

Are you happy with it, @eric-wieser ? let's merge? Thanks!

@kmill
Copy link
Copy Markdown
Collaborator

kmill commented Jul 14, 2023

@bottine I've ported this to leanprover-community/mathlib4#5916

Do you need this in mathlib3 for some reason, or will the mathlib4 version suffice?

@kmill kmill mentioned this pull request Jul 14, 2023
Closed
@0art0
Copy link
Copy Markdown
Collaborator

0art0 commented Jul 15, 2023

@kmill Thank you very much. I suppose the Mathlib4 version suffices, but I'll wait for @bottine to confirm this too.

@bottine
Copy link
Copy Markdown
Collaborator Author

bottine commented Jul 15, 2023

Oh, thanks a lot for porting it! No need for the mathlib3 version.

@eric-wieser eric-wieser added the not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 label Jul 15, 2023
@kmill
Copy link
Copy Markdown
Collaborator

kmill commented Jul 15, 2023

Great! Then I'll close this PR

@kmill kmill closed this Jul 15, 2023
@YaelDillies YaelDillies deleted the bottine/simple_graph.ends/infinite branch July 15, 2023 15:46
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jul 21, 2023
@kmill @ocfnash
feat: infinite (preconnected, locally finite) graphs have nonempty en…
e11c53b 
…ds (#5916)

Port/review of [mathlib#18410](leanprover-community/mathlib3#18410) directly to Mathlib4.

Co-authored-by: Rémi Bottinelli <remi.bottinelli@bluewin.ch>
Co-authored-by: Anand Rao <anand.rao.art@gmail.com>



Co-authored-by: Oliver Nash <github@olivernash.org>
fgdorais pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jul 25, 2023
@kmill @ocfnash @fgdorais
feat: infinite (preconnected, locally finite) graphs have nonempty en…
ce52525 
…ds (#5916)

Port/review of [mathlib#18410](leanprover-community/mathlib3#18410) directly to Mathlib4.

Co-authored-by: Rémi Bottinelli <remi.bottinelli@bluewin.ch>
Co-authored-by: Anand Rao <anand.rao.art@gmail.com>



Co-authored-by: Oliver Nash <github@olivernash.org>
kim-em pushed a commit to leanprover-community/mathlib4 that referenced this pull request Aug 14, 2023
@kmill @ocfnash @kim-em
feat: infinite (preconnected, locally finite) graphs have nonempty en…
f5f1b34 
…ds (#5916)

Port/review of [mathlib#18410](leanprover-community/mathlib3#18410) directly to Mathlib4.

Co-authored-by: Rémi Bottinelli <remi.bottinelli@bluewin.ch>
Co-authored-by: Anand Rao <anand.rao.art@gmail.com>



Co-authored-by: Oliver Nash <github@olivernash.org>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

@eric-wieser eric-wieser Awaiting requested review from eric-wieser

3 more reviewers

@kmill kmill kmill left review comments

@alreadydone alreadydone alreadydone left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

awaiting-review The author would like community review of the PR modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 t-combinatorics Combinatorics

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

7 participants

@bottine @kmill @0art0 @eric-wieser @alreadydone @YaelDillies @kim-em