Definition df-gpg

Description: Definition of generalized Petersen graphs according to Wikipedia "Generalized Petersen graph", 26-Aug-2025, https://en.wikipedia.org/wiki/Generalized_Petersen_graph : "In Watkins' notation, G ( n , k ) is a graph with vertex set { u_0, u_1, ... , u_n-1, v_0, v_1, ... , v_n-1 } and edge set { u_i u_i+1 , u_i v_i , v_i v_i+k | 0 <_ i <_ ( n - 1 ) } where subscripts are to be read modulo n and where k < ( n / 2 ) . Some authors use the notation GPG(n,k)."

Instead of n e. NN , we could restrict the first argument to n e. ( ZZ>=3 ) (i.e., 3 <_ n ), because for n <_ 2 , the definition is not meaningful (since then ( |^( n / 2 ) ) <_ 1 and therefore ( 1 ..^ ( |^( n / 2 ) ) ) = (/) , so that there would be no fitting second argument). (Contributed by AV, 26-Aug-2025)

	Ref	Expression
Assertion	df-gpg	Could not format assertion : No typesetting found for |- gPetersenGr = ( n e. NN , k e. ( 1 ..^ ( |^ ` ( n / 2 ) ) ) |-> { <. ( Base ` ndx ) , ( { 0 , 1 } X. ( 0 ..^ n ) ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ n ) ) | E. x e. ( 0 ..^ n ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } ) } ) >. } ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgpg	Could not format gPetersenGr : No typesetting found for class gPetersenGr with typecode class
1		vn	$$setvarn$$
2		cn	$$class\mathbb{N}$$
3		vk	$$setvark$$
4		c1	$$class1$$
5		cfzo	$$class..^$$
6		cceil	$$class⌈.⌉$$
7	1	cv	$$setvarn$$
8		cdiv	$$class÷$$
9		c2	$$class2$$
10	7 9 8	co	$$class\left(\frac{n}{2}\right)$$
11	10 6	cfv	$$class⌈\frac{n}{2}⌉$$
12	4 11 5	co	$$class\left(1..^⌈\frac{n}{2}⌉\right)$$
13		cbs	$$class\mathrm{Base}$$
14		cnx	$$class\mathrm{ndx}$$
15	14 13	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
16		cc0	$$class0$$
17	16 4	cpr	$$class\left\{0,1\right\}$$
18	16 7 5	co	$$class\left(0..^n\right)$$
19	17 18	cxp	$$class\left(\left\{0,1\right\}\times \left(0..^n\right)\right)$$
20	15 19	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}\times \left(0..^n\right)⟩$$
21		cedgf	$$class\mathrm{ef}$$
22	14 21	cfv	$$class\mathrm{ef}\left(\mathrm{ndx}\right)$$
23		cid	$$class\mathrm{I}$$
24		ve	$$setvare$$
25	19	cpw	$$class𝒫\left(\left\{0,1\right\}\times \left(0..^n\right)\right)$$
26		vx	$$setvarx$$
27	24	cv	$$setvare$$
28	26	cv	$$setvarx$$
29	16 28	cop	$$class⟨0,x⟩$$
30		caddc	$$class+$$
31	28 4 30	co	$$class\left(x+1\right)$$
32		cmo	$$class\mathrm{mod}$$
33	31 7 32	co	$$class\left(\left(x+1\right)\mathrm{mod}n\right)$$
34	16 33	cop	$$class⟨0,\left(x+1\right)\mathrm{mod}n⟩$$
35	29 34	cpr	$$class\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}$$
36	27 35	wceq	$$wffe=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}$$
37	4 28	cop	$$class⟨1,x⟩$$
38	29 37	cpr	$$class\left\{⟨0,x⟩,⟨1,x⟩\right\}$$
39	27 38	wceq	$$wffe=\left\{⟨0,x⟩,⟨1,x⟩\right\}$$
40	3	cv	$$setvark$$
41	28 40 30	co	$$class\left(x+k\right)$$
42	41 7 32	co	$$class\left(\left(x+k\right)\mathrm{mod}n\right)$$
43	4 42	cop	$$class⟨1,\left(x+k\right)\mathrm{mod}n⟩$$
44	37 43	cpr	$$class\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}$$
45	27 44	wceq	$$wffe=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}$$
46	36 39 45	w3o	$$wff\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)$$
47	46 26 18	wrex	$$wff\exists x\in \left(0..^n\right)\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)$$
48	47 24 25	crab	$$class\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^n\right)\right)|\exists x\in \left(0..^n\right)\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)\right\}$$
49	23 48	cres	$$class\left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^n\right)\right)|\exists x\in \left(0..^n\right)\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)\right\}}\right)$$
50	22 49	cop	$$class⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^n\right)\right)|\exists x\in \left(0..^n\right)\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)\right\}}⟩$$
51	20 50	cpr	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}\times \left(0..^n\right)⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^n\right)\right)|\exists x\in \left(0..^n\right)\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)\right\}}⟩\right\}$$
52	1 3 2 12 51	cmpo	$$class\left(n\in \mathbb{N},k\in \left(1..^⌈\frac{n}{2}⌉\right)⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0,1\right\}\times \left(0..^n\right)⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(\left\{0,1\right\}\times \left(0..^n\right)\right)|\exists x\in \left(0..^n\right)\left(e=\left\{⟨0,x⟩,⟨0,\left(x+1\right)\mathrm{mod}n⟩\right\}\vee e=\left\{⟨0,x⟩,⟨1,x⟩\right\}\vee e=\left\{⟨1,x⟩,⟨1,\left(x+k\right)\mathrm{mod}n⟩\right\}\right)\right\}}⟩\right\}\right)$$
53	0 52	wceq	Could not format gPetersenGr = ( n e. NN , k e. ( 1 ..^ ( |^ ` ( n / 2 ) ) ) |-> { <. ( Base ` ndx ) , ( { 0 , 1 } X. ( 0 ..^ n ) ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ n ) ) | E. x e. ( 0 ..^ n ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } ) } ) >. } ) : No typesetting found for wff gPetersenGr = ( n e. NN , k e. ( 1 ..^ ( |^ ` ( n / 2 ) ) ) |-> { <. ( Base ` ndx ) , ( { 0 , 1 } X. ( 0 ..^ n ) ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( { 0 , 1 } X. ( 0 ..^ n ) ) | E. x e. ( 0 ..^ n ) ( e = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod n ) >. } \/ e = { <. 0 , x >. , <. 1 , x >. } \/ e = { <. 1 , x >. , <. 1 , ( ( x + k ) mod n ) >. } ) } ) >. } ) with typecode wff