Skip to content

[Merged by Bors] - feat: infinite (preconnected, locally finite) graphs have nonempty ends#5916

Closed
kmill wants to merge 4 commits intomasterfrom
port/bottine/simple_graph.ends/infinite
Closed

[Merged by Bors] - feat: infinite (preconnected, locally finite) graphs have nonempty ends#5916
kmill wants to merge 4 commits intomasterfrom
port/bottine/simple_graph.ends/infinite

Conversation

@kmill
Copy link
Copy Markdown
Contributor

@kmill kmill commented Jul 14, 2023

Port/review of mathlib#18410 directly to Mathlib4.

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


Open in Gitpod

kmill and others added 2 commits July 14, 2023 21:41
Port/review of mathlib#18410 directly to mathlib4.

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

@ocfnash ocfnash left a comment

Choose a reason for hiding this comment

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

Thanks!

@ocfnash
Copy link
Copy Markdown
Contributor

ocfnash commented Jul 21, 2023

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 21, 2023
bors bot pushed a commit that referenced this pull request Jul 21, 2023
…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>
@bors
Copy link
Copy Markdown

bors bot commented Jul 21, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: infinite (preconnected, locally finite) graphs have nonempty ends [Merged by Bors] - feat: infinite (preconnected, locally finite) graphs have nonempty ends Jul 21, 2023
@bors bors bot closed this Jul 21, 2023
@bors bors bot deleted the port/bottine/simple_graph.ends/infinite branch July 21, 2023 13:02
fgdorais pushed a commit that referenced this pull request Jul 25, 2023
…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 that referenced this pull request Aug 14, 2023
…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 join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants