Star graphs and two locally isomorphic generalized Petersen graphs. #5028
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
* ~bianim, ~fzne1 moved from mathboxes to main * new theorems ~fzdif1, ~fz0dif1, ~fz01pr about integer ranges in main * definition ~df-stgr of star graphs an basic theorems in AV's mathbox
* ~elunsn moved from TA's mathbox to main * new theorem ~f1ounsn in main * new theorems ~elclnbgrelnbgr, ~isubgredgss, ~isubgredg in AV's mathbox * isomorphism between closed neighborhoods and star graphs: ~isubgr3stgr and lemmas
~clnbgr3stgrgrlic added to AV's mathbox
* auxiliary theorems aboz´t generalized Petersen graphs: ~gpgorder, ~gpg5order, ~gpg5gricstgr3 * main theorem ~gpg5grlic
savask
approved these changes
Sep 30, 2025
set.mm
Outdated
| ( cvv wcel csn wrex wb rexsng ax-mp ) DGHACDIJBKEABCDGFLM $. | ||
| $} | ||
|
|
||
| $( Elementhood to a union with a singleton. (Contributed by Thierry Arnoux, |
| ${ | ||
| $d e n x $. | ||
| $( Definition of star graphs according to the first definition in | ||
| Wikipedia, so that ` ( StarGr `` N ) ` has size ` N ` , and order |
There was a problem hiding this comment.
"Size N and order N+1" is very confusing in my opinion, since usually "size" and "order" mean the same thing for other structures (for example, for groups these are synonyms). Maybe it's better to be more precise and say something like "... so that ( StarGr `` N ) has N+1 vertices and N edges ...".
There was a problem hiding this comment.
I think the naming is precise: it is clearly defined in the glossary contained in the chapter header: https://us.metamath.org/mpeuni/mmtheorems290.html#mm28997h. And this is according to literature. So I would like not to change this.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The main result of this PR is ~gpg5grlic, showing that the two generalized Petersen graphs G(N,K) of order 10 (N = 5), which are the Petersen graph G(5,2) and the 5-prism G(5,1), are locally isomorphic. This is the first part of the (new) example to prove the existence of two graphs which are not isomorphic, but locally isomorphic, see issue #4808.
To prove the local isomorphism, star graphs are defined, and the criterion ~clnbgr3stgrgrlic (if all closed neighborhoods of the vertices in two simple graphs with the same order induce a subgraph which is isomorphic to an N-star, then the two graphs are locally isomorphic) is used. This criterion is based on the fact that if a vertex of a simple graph has exactly N (different) neighbors, and none of these neighbors are connected by an edge, then the closed neighborhood of this vertex induces a subgraph which is isomorphic to an N-star (see ~isubgr3stgr).
Besides these three main results, some auxiliary theorems (in main and my mathbox) are provided.