diff --git a/changes-set.txt b/changes-set.txt index cd6f987b9b..28ed6a408a 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -93,6 +93,9 @@ make a github issue.) DONE: Date Old New Notes 1-Oct-25 inindif [same] Moved from TA's mathbox to main set.mm +29-Sep-25 elunsn [same] moved from TA's mathbox to main set.mm +29-Sep-25 bianim [same] moved from PM's mathbox to main set.mm +29-Sep-25 fzne1 [same] moved from TA's mathbox to main set.mm 23-Sep-25 coecj [same] Removed unneeded hypothesis 23-Sep-25 plycj [same] Removed unneeded hypothesis 23-Sep-25 elfzolem1 [same] moved from GS's mathbox to main set.mm diff --git a/set.mm b/set.mm index 80cc5b7c02..f9421d9da0 100644 --- a/set.mm +++ b/set.mm @@ -5307,6 +5307,15 @@ use disjunction (although this is not required since definitions are ( wa pm5.32i ancom 3bitr4i ) ABEACEBAECAEABCDFBAGCAGH $. $} + ${ + bianim.1 $e |- ( ph <-> ( ps /\ ch ) ) $. + bianim.2 $e |- ( ch -> ( ps <-> th ) ) $. + $( Exchanging conjunction in a biconditional. (Contributed by Peter Mazsa, + 31-Jul-2023.) $) + bianim $p |- ( ph <-> ( th /\ ch ) ) $= + ( wa pm5.32ri bitri ) ABCGDCGECBDFHI $. + $} + ${ pm5.32d.1 $e |- ( ph -> ( ps -> ( ch <-> th ) ) ) $. $( Distribution of implication over biconditional (deduction form). @@ -44456,6 +44465,13 @@ will do (e.g., ` O = (/) ` and ` T = { (/) } ` , see ~ 0nep0 ). ( cvv wcel csn wrex wb rexsng ax-mp ) DGHACDIJBKEABCDGFLM $. $} + $( Elementhood in a union with a singleton. (Contributed by Thierry Arnoux, + 14-Dec-2023.) $) + elunsn $p |- ( A e. V -> ( A e. ( B u. { C } ) <-> ( A e. B \/ A = C ) ) ) + $= + ( csn cun wcel wo wceq elun elsng orbi2d bitrid ) ABCEZFGABGZANGZHADGZOACIZ + HABNJQPROACDKLM $. + ${ $d x A $. $d x B $. $d x C $. $( Membership in an extension of a power class. (Contributed by NM, @@ -70203,6 +70219,54 @@ more bytes (305 versus 282). (Contributed by AV, 3-Feb-2021.) MABCDEPUJULUCUIUKACUIUEUDIZUGKZBCLUKUHUNBCUFUMUGUDUEQRSUGBCUDUATSUBT $. $} + ${ + $d A a b x y $. $d B x y $. $d G a b x y $. $d V x y $. $d W x y $. + $d X x y $. $d Y x y $. + f1ounsn.f $e |- F = ( G u. { <. X , Y >. } ) $. + $( Extension of a bijection by an ordered pair. (Contributed by AV, + 15-Sep-2025.) $) + f1ounsn $p |- ( ( G : A -1-1-onto-> B /\ ( X e. V /\ Y e. W ) + /\ ( X e/ A /\ Y e/ B ) ) + -> F : ( A u. { X } ) -1-1-onto-> ( B u. { Y } ) ) $= + ( vx vy wcel wa wne cfv wi wral wceq adantr syl wf1o wnel w3a csn cun cop + va vb wf cv crn wn f1of wss ssun1 a1i fssd 3ad2ant1 df-nel biimpi anim12i + simpl 3adant1 wo eqid olci elunsn mpbiri adantl 3ad2ant2 fsnunf wf1 f1of1 + 3jca dff14a weq neeq1 fveq2 neeq1d imbi12d neeq2 neeq2d expcom sylbi impl + rspc2va imp nelne2 necomd 3ad2ant3 fvunsn 3netr4d ex ralrimiva ffvelcdmda + syl2anc simpr f1odm eqcomd eleq2d notbid bitrid biimpd adantrd 3adant2 wb + cdm fsnunfv ralsng mpbird ralun jca eqneqall ax-mp ralbidv rnun wfo f1ofo + forn rnsnopg uneq12d eqtrid dff1o5 bianbi sylibr f1oeq1 ) ABDUAZGELZHFLZM + ZGAUBZHBUBZMZUCZAGUDZUEZBHUDZUEZDGHUFUDZUEZUAZYPYRCUAZYNYPYRYTUIZJUJZKUJZ + NZUUDYTOZUUEYTOZNZPZKYPQZJYPQZMZYTUKZYRRZMUUAYNUUMUUOYNUUCUULYNAYRDUIZYHG + ALZULZMZHYRLZUCUUCYNUUPUUSUUTYGYJUUPYMYGABYRDABDUMZBYRUNYGBYQUOUPUQURYJYM + UUSYGYJYHYMUURYHYIVBZYKUURYLYKUURGAUSZUTSVAVCYJYGUUTYMYIUUTYHYIUUTHBLZHHR + ZVDUVEUVDHVEVFHBHFVGVHVIVJVNAYRDEGHVKTYNUUKJAQUUKJYOQZUULYNUUKJAYNUUDALZM + ZUUJKAQUUJKYOQZUUKUVHUUJKAUVHUUEALZMZUUFUUIUVKUUFMZUUDDOZUUEDOZUUGUUHUVKU + UFUVMUVNNZYNUVGUVJUUFUVOPZYGYJUVGUVJMZUVPPZYMYGABDVLZUVRABDVMUVSABDUIZUGU + JZUHUJZNZUWADOZUWBDOZNZPZUHAQUGAQZMUVRUGUHABDVOUWHUVRUVTUVQUWHUVPUWGUVPUU + DUWBNZUVMUWENZPUGUHUUDUUEAAUGJVPZUWCUWIUWFUWJUWAUUDUWBVQUWKUWDUVMUWEUWAUU + DDVRVSVTUHKVPZUWIUUFUWJUVOUWBUUEUUDWAUWLUWEUVNUVMUWBUUEDVRWBVTWFWCVIWDTUR + WEWGUVLGUUDNZUUGUVMRZUVKUWMUUFUVHUWMUVJYNUVGUWMYMYGUVGUWMPZYJYKUWOYLYKUUR + UWOUVCUVGUURUWMUVGUURMUUDGUUDGAWHWIWCWDSWJWGSSDGHUUDWKZTUVLGUUENZUUHUVNRZ + UVKUWQUUFUVHUVJUWQYNUVJUWQPZUVGYMYGUWSYJYKUWSYLYKUURUWSUVCUVJUURUWQUVJUUR + MUUEGUUEGAWHWIWCWDSWJSWGSDGHUUEWKZTWLWMWNUVHUVIUUDGNZUUGGYTOZNZPZUVHUXAUX + CUVHUXAMZUVMHUUGUXBUVHUVMHNZUXAUVHUVMBLUVDULZUXFYNABUUDDYGYJUVTYMUVAURZWO + YNUXGUVGYMYGUXGYJYLUXGYKYLUXGHBUSUTVIWJZSUVMHBWHWPSUXEUWMUWNUXEUUDGUVHUXA + WQWIUWPTUXEYHYIGDXGZLZULZUCZUXBHRZUVHUXMUXAYNUXMUVGYNYHYIUXLYJYGYHYMUVBVJ + ZYJYGYIYMYHYIWQVJYGYMUXLYJYGYMUXLYGYKUXLYLYGYKUXLYKUURYGUXLUVCYGUUQUXKYGA + UXJGYGUXJAABDWRWSWTXAXBXCXDWGXEVNZSSDEFGHXHZTWLWMUVHYHUVIUXDXFYNYHUVGUXOS + UUJUXDKGEUUEGRZUUFUXAUUIUXCUUEGUUDWAUXRUUHUXBUUGUUEGYTVRZWBVTXITXJUUJKAYO + XKWPWNYNUVFUWQUXBUUHNZPZKYPQZYNUYAKAQUYAKYOQZUYBYNUYAKAYNUVJMZUWQUXTUYDUW + QMZHUVNUXBUUHUYEUVNBLZUXGMZHUVNNUYDUYGUWQUYDUYFUXGYNABUUEDUXHWOYNUXGUVJUX + ISXLSUYGUVNHUVNHBWHWITUYEUXMUXNUYDUXMUWQYNUXMUVJUXPSSUXQTUWQUWRUYDUWTVIWL + WMWNYNUYCGGNZUXBUXBNZPZGGRUYJGVEUYIGGXMXNYNYHUYCUYJXFUXOUYAUYJKGEUXRUWQUY + HUXTUYIUUEGGWAUXRUUHUXBUXBUXSWBVTXITVHUYAKAYOXKWPYNYHUVFUYBXFUXOUUKUYBJGE + UUDGRZUUJUYAKYPUYKUUFUWQUUIUXTUUDGUUEVQUYKUUGUXBUUHUUDGYTVRVSVTXOXITXJUUK + JAYOXKWPXLYNUUNDUKZYSUKZUEYRDYSXPYNUYLBUYMYQYGYJUYLBRZYMYGABDXQUYNABDXRAB + DXSTURYJYGUYMYQRZYMYHUYOYIGHEXTSVJYAYBXLUUAYPYRYTVLUUOUUMYPYRYTYCJKYPYRYT + VOYDYECYTRUUBUUAXFIYPYRCYTYFXNYE $. + $} + ${ $d x y A $. $d x y F $. $d x y X $. $d x y Y $. f12dfv.a $e |- A = { X , Y } $. @@ -149546,6 +149610,39 @@ subset of a (possibly extended) finite sequence of integers. (Contributed OUSULUSUOBMFCBDQABMSRTUQUSULAUPOPUAULUNABUBZFZUQLZUSURULUNAVAUPUCZFVCULUMVD ABCUDUEAVAUPUJUFUSVBUOUQABMUGUKUHUI $. + $( Elementhood in a finite set of sequential integers, except its lower + bound. (Contributed by Thierry Arnoux, 1-Jan-2024.) $) + fzne1 $p |- ( ( K e. ( M ... N ) /\ K =/= M ) + -> K e. ( ( M + 1 ) ... N ) ) $= + ( wne cfz co wcel wceq wn c1 caddc df-ne wo cuz cfv elfzuz2 elfzp12 syl ibi + wb orcanai sylan2b ) ABDABCEFGZABHZIABJKFCEFGZABLUCUDUEUCUDUEMZUCCBNOGUCUFT + ABCPABCQRSUAUB $. + + ${ + $d M x $. $d N x $. + $( Split the first element of a finite set of sequential integers. More + generic than ~ fzpred . Analogous to ~ fzdif2 . (Contributed by AV, + 12-Sep-2025.) $) + fzdif1 $p |- ( N e. ( ZZ>= ` M ) + -> ( ( M ... N ) \ { M } ) = ( ( M + 1 ) ... N ) ) $= + ( vx cuz cfv wcel cfz co csn cdif c1 caddc cv wn wa cz cle wbr wi ex 3syl + eldif wne elsng necon3bbid fzne1 sylbida wss eluzel2 uzidd peano2uz fzss1 + sselda w3a elfz2 cr adantl clt wb simp3 zltp1le syl2anr biimprd a1d com24 + zred imp42 gtned sylbi impcom nelsn syl jca impbid2 bitrid eqrdv ) BADEZF + ZCABGHZAIZJZAKLHZBGHZCMZWAFWDVSFZWDVTFZNZOZVRWDWCFZWDVSVTUBVRWHWIWEWGWDAU + CZWIWEWFWDAWDAVSUDUEWDABUFUGVRWIWHVRWIOZWEWGVRWCVSWDVRAVQFWBVQFWCVSUHVRAA + BUIZUJAAUKWBABULUAUMWKWJWGWIVRWJWIWBPFZBPFZWDPFZUNZWBWDQRZWDBQRZOOZVRWJSW + DWBBUOWSVRWJWSVROAWDVRAUPFWSVRAWLVFUQWPWQWRVRAWDURRZWPVRWRWQWTWPVRWRWQWTS + ZSWPVROZXAWRXBWTWQVRAPFWOWTWQUSWPWLWMWNWOUTAWDVAVBVCVDTVEVGVHTVIVJWDAVKVL + VMTVNVOVP $. + $} + + $( Split the first element of a finite set of sequential nonnegative + integers. (Contributed by AV, 12-Sep-2025.) $) + fz0dif1 $p |- ( N e. NN0 -> ( ( 0 ... N ) \ { 0 } ) = ( 1 ... N ) ) $= + ( cn0 wcel cc0 cfz co csn cdif c1 caddc cuz wceq elnn0uz fzdif1 sylbi 0p1e1 + cfv oveq1i eqtrdi ) ABCZDAEFDGHZDIJFZAEFZIAEFTADKQCUAUCLAMDANOUBIAEPRS $. + $( Choices for an element of a finite interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) $) fzm1 $p |- ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... N ) <-> @@ -150941,6 +151038,12 @@ Finite intervals of nonnegative integers (or "finite sets of sequential cpr eqtr4i oveq2i 0z fzpr preq2i eqtrdi 3eqtri ) ABCDZABEFDZGDZAAEHDZGDZAEQ ZBIJUEUGKLABMNUFUHAGUFEUHOPRSAIJZUIUJKTUKUIAUHQUJAUAUHEAPUBUCNUD $. + $( An integer range between 0 and 1 is a pair. (Contributed by AV, + 11-Sep-2025.) $) + fz01pr $p |- ( 0 ... 1 ) = { 0 , 1 } $= + ( cc0 c1 cfz co caddc cpr 1e0p1 oveq2i cz wcel wceq fzpr ax-mp 0p1e1 preq2i + 0z 3eqtri ) ABCDAABEDZCDZARFZABFBRACGHAIJSTKPALMRBANOQ $. + $( A half-open integer range from 0 to 3 is an unordered triple. (Contributed by Alexander van der Vekens, 9-Nov-2017.) $) fzo0to3tp $p |- ( 0 ..^ 3 ) = { 0 , 1 , 2 } $= @@ -481388,6 +481491,9 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the htmldef "GrTriangles" as "GrTriangles"; althtmldef "GrTriangles" as "GrTriangles"; latexdef "GrTriangles" as "\mathrm{GrTriangles}"; +htmldef "StarGr" as "StarGr"; + althtmldef "StarGr" as "StarGr"; + latexdef "StarGr" as "\mathrm{StarGr}"; htmldef "GraphLocIso" as " GraphLocIso "; althtmldef "GraphLocIso" as " GraphLocIso "; latexdef "GraphLocIso" as "\mathrm{GraphLocIso}"; @@ -502632,13 +502738,6 @@ Class abstractions (a.k.a. class builders) -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- $) - $( Elementhood to a union with a singleton. (Contributed by Thierry Arnoux, - 14-Dec-2023.) $) - elunsn $p |- ( A e. V -> ( A e. ( B u. { C } ) <-> ( A e. B \/ A = C ) ) ) - $= - ( csn cun wcel wo wceq elun elsng orbi2d bitrid ) ABCEZFGABGZANGZHADGZOACIZ - HABNJQPROACDKLM $. - $( Negated membership for a union. (Contributed by Thierry Arnoux, 13-Dec-2023.) $) nelun $p |- ( A = ( B u. C ) -> ( -. X e. A <-> ( -. X e. B /\ -. X e. C ) @@ -506987,14 +507086,6 @@ its graph has a given second element (that is, function value). EIKUHUIUOWIWK $. $} - $( Elementhood in a finite set of sequential integers, except its lower - bound. (Contributed by Thierry Arnoux, 1-Jan-2024.) $) - fzne1 $p |- ( ( K e. ( M ... N ) /\ K =/= M ) -> K e. ( ( M + 1 ) ... N ) ) - $= - ( wne cfz co wcel wceq wn c1 caddc df-ne wo cuz cfv elfzuz2 elfzp12 syl ibi - wb orcanai sylan2b ) ABDABCEFGZABHZIABJKFCEFGZABLUCUDUEUCUDUEMZUCCBNOGUCUFT - ABCPABCQRSUAUB $. - $( Elementhood of an integer and its predecessor in finite intervals of integers. (Contributed by Thierry Arnoux, 1-Jan-2024.) $) fzm1ne1 $p |- ( ( K e. ( M ... N ) /\ K =/= M ) @@ -616878,15 +616969,6 @@ A collection of theorems for commuting equalities (or ( wa w3a biantrur 3anass 3bitr4i ) BCFZAKFCABCGAKDHBCEHABCIJ $. $} - ${ - bianim.1 $e |- ( ph <-> ( ps /\ ch ) ) $. - bianim.2 $e |- ( ch -> ( ps <-> th ) ) $. - $( Exchanging conjunction in a biconditional. (Contributed by Peter Mazsa, - 31-Jul-2023.) $) - bianim $p |- ( ph <-> ( th /\ ch ) ) $= - ( wa pm5.32ri bitri ) ABCGDCGECBDFHI $. - $} - ${ biorfd.1 $e |- ( ph -> -. ps ) $. $( A wff is equivalent to its disjunction with falsehood, deduction form. @@ -818031,6 +818113,17 @@ Graph theory (extension) GUHUIUJ $. $} + $( An element of the closed neighborhood of a vertex which is not the vertex + itself is an element of the open neighborhood of the vertex. (Contributed + by AV, 24-Sep-2025.) $) + elclnbgrelnbgr $p |- ( ( X e. ( G ClNeighbVtx N ) /\ X =/= N ) + -> X e. ( G NeighbVtx N ) ) $= + ( cclnbgr co wcel wne cnbgr wi csn cun cvtx cfv wceq clnbgrcl dfclnbgr4 syl + eqid a1i sylbid eleq2d elun elsng eqneqall ax-1 jaod biimtrid pm2.43i imp + wo ) CABDEZFZCBGZCABHEZFZULUMUOIZULULCBJZUNKZFZUPULUKURCULBALMZFUKURNACUTBU + TRZOABUTVAPQUAUSCUQFZUOUJULUPCUQUNUBULVBUPUOULVBCBNZUPCBUKUCVCUPIULUOCBUDST + UOUPIULUOUMUESUFUGTUHUI $. + ${ $d G e n $. $d I e i n $. $d N e i n $. $d V e n $. dfclnbgr3.v $e |- V = ( Vtx ` G ) $. @@ -818530,6 +818623,50 @@ graph that join vertices of the subgraph (see section I.1 in [Bollobas] GVHVPVEAUNVRVFCVFVNVOUOUPTUQURTAVIUSUTVAVB $. $} + ${ + $d G x $. $d S x $. $d V x $. + isubgredg.v $e |- V = ( Vtx ` G ) $. + isubgredg.e $e |- E = ( Edg ` G ) $. + isubgredg.h $e |- H = ( G ISubGr S ) $. + isubgredg.i $e |- I = ( Edg ` H ) $. + $( The edges of an induced subgraph of a graph are edges of the graph. + (Contributed by AV, 24-Sep-2025.) $) + isubgredgss $p |- ( ( G e. W /\ S C_ V ) -> I C_ E ) $= + ( vx wcel wss ciedg cfv crn cedg edgval eqtri wa cv cdm crab cres cisubgr + co fveq2i eqid isubgriedg eqtrid rneqd resss rnss mp1i eqsstrd 3sstr4g ) + CGMAFNUAZDOPZQZCOPZQZEBURUTVALUBVAPANLVAUCUDZUEZQZVBURUSVDURUSCAUFUGZOPVD + DVFOJUHLAVACFGHVAUIUJUKULVDVANVEVBNURVAVCUMVDVAUNUOUPEDRPUTKDSTBCRPVBICST + UQ $. + + $d G i x $. $d K x $. $d S i $. $d V i $. + $( An edge of an induced subgraph of a hypergraph is an edge of the + hypergraph connecting vertices of the subgraph. (Contributed by AV, + 24-Sep-2025.) $) + isubgredg $p |- ( ( G e. UHGraph /\ S C_ V ) + -> ( K e. I <-> ( K e. E /\ K C_ S ) ) ) $= + ( vi vx wcel wss wa ciedg cfv wceq adantr cuhgr crn cv cdm crab cres wrex + cisubgr co fveq2i eqid isubgriedg eqtrid rneqd eleq2d wfn wb cpw csn cdif + c0 wf uhgrf ffnd ssrab2 a1i fnssresd fvelrnb fvres adantl eqeq1d wi fveq2 + syl weq sseq1d elrab wfun uhgrfun simpl fvelrn syl2anr simpr jca ex sylbi + impcom eleq1 anbi12d syl5ibcom sylbid rexlimdva cedg edgval eqcomi eleq2i + sseq1 edgiedgb bitrid wex simprl biimpcd sylanbrc eqcomd sylan9eqr eximdv + imp mpdan df-rex 3imtr4g com23 impd impbid 3bitrd eqtri anbi1i 3bitr4g ) + CUANZAGOZPZFDQRZUBZNZFCQRZUBZNZFAOZPZFENFBNZYGPXTYCFYDLUCZYDRZAOZLYDUDZUE + ZUFZUBZNZMUCZYORZFSZMYNUGZYHXTYBYPFXTYAYOXTYACAUHUIZQRYODUUBQJUJLAYDCGUAH + YDUKZULUMUNUOXTYOYNUPYQUUAUQXTYMYNYDXTYMGURVAUSUTZYDXRYMUUDYDVBXSYDCGHUUC + VCTVDYNYMOXTYLLYMVEVFVGMYNFYOVHVNXTUUAYHXTYTYHMYNXTYRYNNZPZYTYRYDRZFSZYHU + UFYSUUGFUUEYSUUGSXTYRYNYDVIZVJVKUUFUUGYENZUUGAOZPZUUHYHUUEXTUULUUEYRYMNZU + UKPZXTUULVLYLUUKLYRYMLMVOYKUUGAYJYRYDVMVPVQZUUNXTUULUUNXTPUUJUUKXTYDVRZUU + MUUJUUNXRUUPXSYDCUUCVSZTUUMUUKVTYRYDWAWBUUNUUKXTUUMUUKWCTWDWEWFWGUUHUUJYF + UUKYGUUGFYEWHUUGFAWQWIWJWKWLXTYFYGUUAXTYFFUUGSZMYMUGZYGUUAVLXRYFUUSUQZXSX + RUUPUUTUUQYFFCWMRZNUUPUUSYEUVAFUVAYECWNZWOWPMFCYDUUCWRWSVNTXTYGUUSUUAXTYG + UUSUUAVLXTYGPZUUMUURPZMWTUUEYTPZMWTUUSUUAUVCUVDUVEMUVCUVDUVEUVCUVDPZUUEUV + EUVFUUMUUKUUEUVCUUMUURXAUVCUVDUUKYGUVDUUKVLXTUVDYGUUKUVDFUUGAUUMUURWCZVPX + BVJXGUUOXCUVFUUEPUUEYTUVFUUEWCUUEUVFYSUUGFUUIUVDUUHUVCUVDFUUGUVGXDVJXEWDX + HWEXFUURMYMXIYTMYNXIXJWEXKWKXLXMXNEYBFEDWMRYBKDWNXOWPYIYFYGBYEFBUVAYEIUVB + XOWPXPXQ $. + $} + ${ $d G x $. $d S x $. $d V x $. isubgrvtx.v $e |- V = ( Vtx ` G ) $. @@ -820087,6 +820224,462 @@ provide a criterion for two graphs being not isomorphic (see ~ grimgrtri ). $} +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Star graphs +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + + According to Wikipedia "Star (graph theory)", 10-Sep-2025, + ~ https://en.wikipedia.org/wiki/Star_(graph_theory) : "In graph theory, the + star S_k is the complete bipartite graph K(1,k), that is, it is a tree with + one internal node and k leaves. Alternatively, some authors define S_k to + be the tree of order k with maximum diameter 2, in which case a star of + k > 2 has k - 1 leaves.". + +$) + + $c StarGr $. + + $( Extend class notation with star graphs. $) + cstgr $a class StarGr $. + + ${ + $d e n x $. + $( Definition of star graphs according to the first definition in + Wikipedia, so that ` ( StarGr `` N ) ` has size ` N ` , and order + ` N + 1 ` : ` ( StarGr `` 0 ) ` will be a single vertex (graph without + edges), see ~ stgr0 , ` ( StarGr `` 1 ) ` will be a single edge (graph + with two vertices connected by an edge), see ~ stgr1 , and + ` ( StarGr `` 3 ) ` will be a 3-star or "claw" (a star with 3 edges). + (Contributed by AV, 10-Sep-2025.) $) + df-stgr $a |- StarGr = ( n e. NN0 + |-> { <. ( Base ` ndx ) , ( 0 ... n ) >. , + <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... n ) | + E. x e. ( 1 ... n ) e = { 0 , x } } ) >. } ) $. + $} + + ${ + $d N e n x $. + $( The star graph S_N. (Contributed by AV, 10-Sep-2025.) $) + stgrfv $p |- ( N e. NN0 -> ( StarGr ` N ) + = { <. ( Base ` ndx ) , ( 0 ... N ) >. , + <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | + E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } ) $= + ( vn cn0 wcel cnx cfv cc0 cv cfz co cop cid cpr wceq c1 wrex cpw crab cbs + cedgf cres cstgr cvv df-stgr oveq2 opeq2d pweqd rexeqdv rabeqbidv reseq2d + cmpt a1i preq12d adantl id prex fvmptd ) CEFZDCGUAHZIDJZKLZMZGUBHZNBJIAJO + PZAQVBKLZRZBVCSZTZUCZMZOZVAICKLZMZVENVFAQCKLZRZBVNSZTZUCZMZOZEUDUEUDDEVMU + MPUTABDUFUNVBCPZVMWBPUTWCVDVOVLWAWCVCVNVAVBCIKUGZUHWCVKVTVEWCVJVSNWCVHVQB + VIVRWCVCVNWDUIWCVFAVGVPVBCQKUGUJUKULUHUOUPUTUQWBUEFUTVOWAURUNUS $. + $} + + ${ + $d N e x $. + $( The vertices of the star graph S_N. (Contributed by AV, 11-Sep-2025.) $) + stgrvtx $p |- ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) ) $= + ( ve vx cn0 wcel cstgr cfv cvtx cnx cbs cc0 cfz co cop cedgf cpr wceq cvv + cv eqid cid c1 wrex cpw crab cres stgrfv fveq2d ovex pwexg rabexd resiexd + wa ax-mp pm3.2i struct2grvtx mp1i eqtrd ) ADEZAFGZHGIJGKALMZNIOGUABSKCSPQ + CUBALMUCZBVAUDZUEZUFZNPZHGZVAUSUTVFHCBAUGUHVAREZVEREZUMVGVAQUSVHVIKALUIZV + HVIVJVHVDRVHVBBVCVDRVDTVARUJUKULUNUOVEVFVARRVFTUPUQUR $. + + $( The indexed edges of the star graph S_N. (Contributed by AV, + 11-Sep-2025.) $) + stgriedg $p |- ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) + = ( _I |` { e e. ~P ( 0 ... N ) | + E. x e. ( 1 ... N ) e = { 0 , x } } ) ) $= + ( cn0 wcel cstgr cfv ciedg cnx cbs cc0 cfz co cop cedgf cpr wceq cvv eqid + cv cid c1 wrex crab cres stgrfv fveq2d wa ovex pwexg rabexd resiexd ax-mp + cpw pm3.2i struct2griedg mp1i eqtrd ) CDEZCFGZHGIJGKCLMZNIOGUABTKATPQAUBC + LMUCZBVAUNZUDZUEZNPZHGZVEUSUTVFHABCUFUGVAREZVEREZUHVGVEQUSVHVIKCLUIZVHVIV + JVHVDRVHVBBVCVDRVDSVARUJUKULUMUOVEVFVARRVFSUPUQUR $. + + $( The edges of the star graph S_N. (Contributed by AV, 11-Sep-2025.) $) + stgredg $p |- ( N e. NN0 -> ( Edg ` ( StarGr ` N ) ) + = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) $= + ( cn0 wcel cstgr cfv cedg ciedg crn cv cc0 cpr wceq c1 cfz wrex cpw crab + co edgval cid cres stgriedg rneqd rnresi eqtrdi eqtrid ) CDEZCFGZHGUJIGZJ + ZBKLAKMNAOCPTQBLCPTRSZUJUAUIULUBUMUCZJUMUIUKUNABCUDUEUMUFUGUH $. + + $d E e x $. + $( An edge of the star graph S_N. (Contributed by AV, 11-Sep-2025.) $) + stgredgel $p |- ( N e. NN0 -> ( E e. ( Edg ` ( StarGr ` N ) ) + <-> ( E C_ ( 0 ... N ) /\ E. x e. ( 1 ... N ) E = { 0 , x } ) ) ) $= + ( ve cn0 wcel cstgr cfv cedg cv cc0 cpr wceq c1 cfz co wrex cpw crab cvv + wss wa stgredg eleq2d eqeq1 rexbidv elrab wb wi prex eleq1 mpbiri syl a1i + elpwg rexlimiv bianim bitrdi ) CEFZBCGHIHZFBDJZKAJZLZMZANCOPZQZDKCOPZRZSZ + FZBVGUAZBVCMZAVEQZUBUSUTVIBADCUCUDVJBVHFZVMVKVFVMDBVHVABMVDVLAVEVABVCUEUF + UGVLVNVKUHZAVEVLVOUIVBVEFVLBTFZVOVLVPVCTFKVBUJBVCTUKULBVGTUOUMUNUPUQUR $. + + $( The edges of the star graph S_N as indexed union. (Contributed by AV, + 29-Sep-2025.) $) + stgredgiun $p |- ( N e. NN0 -> ( Edg ` ( StarGr ` N ) ) + = U_ x e. ( 1 ... N ) { { 0 , x } } ) $= + ( ve cn0 wcel cstgr cfv cedg c1 cfz co cc0 cv cpr csn wss wrex wa wb a1i + ciun stgredgel eliun velsn 0elfz adantr fz1ssfz0 sseli adantl prssd sseq1 + wceq syl5ibrcom pm4.71rd bitr2id rexbidva r19.42v 3bitr2rd bitrd eqrdv ) + BDEZCBFGHGZAIBJKZLAMZNZOZUAZVACMZVBEVHLBJKZPZVHVEULZAVCQRZVHVGEZAVHBUBVAV + MVHVFEZAVCQZVJVKRZAVCQZVLVMVOSVAAVHVCVFUCTVAVPVNAVCVNVKVAVDVCEZRZVPCVEUDV + SVKVJVSVJVKVEVIPVSLVDVIVALVIEVRBUEUFVRVDVIEVAVCVIVDBUGUHUIUJVHVEVIUKUMUNU + OUPVQVLSVAVJVKAVCUQTURUSUT $. + $} + + ${ + $d N e k x $. + $( The star graph S_N is a simple graph. (Contributed by AV, + 11-Sep-2025.) $) + stgrusgra $p |- ( N e. NN0 -> ( StarGr ` N ) e. USGraph ) $= + ( ve vx vk wcel cstgr cfv cdm cv chash wceq cpw crab wf1 cc0 cfz mp1i cvv + c2 wa cn0 cusgr ciedg cvtx cpr c1 co wrex cid cres wss wf1o f1of1 simpllr + f1oi fveq2 wne 0red elfznn nngt0d ltned wb c0ex vex pm3.2i hashprg adantl + mpbid sylan9eqr jca rexlimdva expimpd eqeq1 rexbidv elrab fveqeq2 3imtr4g + weq ssrdv f1ss syl2anc stgriedg dmeqd dmresi eqtrdi stgrvtx pweqd rabeqdv + ex f1eq123d mpbird fvex eqid isusgrs ) AUAEZAFGZUBEZWPUCGZHZBIZJGSKZBWPUD + GZLZMZWRNZWOXEWTOCIZUEZKZCUFAPUGZUHZBOAPUGZLZMZXABXLMZUIXMUJZNZWOXMXMXONZ + XMXNUKXPXMXMXOULXQWOXMUOXMXMXOUMQWODXMXNWODIZXLEZXRXGKZCXIUHZTXSXRJGZSKZT + ZXRXMEXRXNEWOXSYAYDWOXSTZXTYDCXIYEXFXIEZTZXTYDYGXTTXSYCWOXSYFXTUNXTYGYBXG + JGZSXRXGJUPYFYHSKZYEYFOXFUQZYIYFOXFYFURYFXFXFAUSUTVAOREZXFREZTYJYIVBYFYKY + LVCCVDVEOXFRRVFQVHVGVIVJWIVKVLXJYABXRXLBDVRXHXTCXIWTXRXGVMVNVOXAYCBXRXLWT + XRSJVPVOVQVSXMXMXNXOVTWAWOWSXMXDXNWRXOCBAWBZWOWSXOHXMWOWRXOYMWCXMWDWEWOXA + BXCXLWOXBXKAWFWGWHWJWKWPREWQXEVBWOAFWLBRWRWPXBXBWMWRWMWNQWK $. + $} + + ${ + $d e x $. + $( The star graph S_0 consists of a single vertex without edges. + (Contributed by AV, 11-Sep-2025.) $) + stgr0 $p |- ( StarGr ` 0 ) = { <. ( Base ` ndx ) , { 0 } >. , + <. ( .ef ` ndx ) , (/) >. } $= + ( ve vx cc0 cstgr cfv cnx cbs cfz co cop cid cv cpr wceq cres wcel opeq2i + c0 wn eqtri cedgf c1 wrex cpw crab csn cn0 0nn0 stgrfv ax-mp fz0sn rabeq0 + wral wi noel pm2.21i fz10 eleq2s a1i ralrimiv ralnex mprgbir reseq2i res0 + sylib preq12i ) CDEZFGEZCCHIZJZFUAEZKALZCBLZMNZBUBCHIZUCZAVIUDZUEZOZJZMZV + HCUFZJZVKRJZMCUGPVGWANUHBACUIUJVJWCVTWDVIWBVHUKQVSRVKVSKRORVRRKVRRNVPSZAV + QVPAVQULVLVQPZVNSZBVOUMWEWFWGBVOVMVOPWGUNWFWGVMRVOVMRPWGVMUOUPUQURUSUTVNB + VOVAVEVBVCKVDTQVFT $. + + $( The star graph S_1 consists of a single simple edge. (Contributed by + AV, 11-Sep-2025.) $) + stgr1 $p |- ( StarGr ` 1 ) = { <. ( Base ` ndx ) , { 0 , 1 } >. , + <. ( .ef ` ndx ) , ( _I |` { { 0 , 1 } } ) >. } $= + ( ve vx c1 cfv cnx cc0 cfz co cop cid cpr wceq wrex cres csn ax-mp fz01pr + cv wcel opeq2i cstgr cbs cedgf cpw crab cn0 1nn0 stgrfv wa wi elsni preq2 + cab eqeq2d biimpd syl cz 1z fzsn eleq2s rexlimiv adantl c0ex eleqtrri 1ex + prid1 prid2 prelpwi mp2an rexeqi rexsn bitri mpbir pm3.2i rexbidv anbi12d + eqid eleq1 eqeq1 mpbiri impbii abbii df-rab df-sn 3eqtr4i reseq2i preq12i + eqtri ) CUADZEUBDZFCGHZIZEUCDZJARZFBRZKZLZBCCGHZMZAWKUDZUEZNZIZKZWJFCKZIZ + WMJXEOZNZIZKCUFSWIXDLUGBACUHPWLXFXCXIWKXEWJQTXBXHWMXAXGJWNWTSZWSUIZAUMWNX + ELZAUMXAXGXKXLAXKXLWSXLXJWQXLBWRWQXLUJZWOCOZWRWOXNSWOCLZXMWOCUKXOWQXLXOWP + XEWNWOCFULZUNUOUPCUQSWRXNLURCUSPZUTVAVBXLXKXEWTSZXEWPLZBWRMZUIXRXTFWKSCWK + SXRFXEWKFCVCVFQVDCXEWKFCVEVGQVDFCWKVHVIXTXEXELZXEVQXTXSBXNMYAXSBWRXNXQVJX + SYABCVEXOWPXEXEXPUNVKVLVMVNXLXJXRWSXTWNXEWTVRXLWQXSBWRWNXEWPVSVOVPVTWAWBW + SAWTWCAXEWDWEWFTWGWH $. + $} + + ${ + stgrvtx0.g $e |- G = ( StarGr ` N ) $. + stgrvtx0.v $e |- V = ( Vtx ` G ) $. + $( The center ("internal node") of a star graph S_N. (Contributed by AV, + 12-Sep-2025.) $) + stgrvtx0 $p |- ( N e. NN0 -> 0 e. V ) $= + ( cn0 wcel cstgr cfv cvtx cc0 cfz co wceq fveq2i eqtri eqeq1i 0elfz eleq2 + stgrvtx syl5ibrcom biimtrrid mpd ) BFGZBHIZJIZKBLMZNZKCGZBTUHCUGNZUDUICUF + UGCAJIUFEAUEJDOPQUDUIUJKUGGBRCUGKSUAUBUC $. + + $( The order of a star graph S_N. (Contributed by AV, 12-Sep-2025.) $) + stgrorder $p |- ( N e. NN0 -> ( # ` V ) = ( N + 1 ) ) $= + ( cn0 wcel chash cfv cc0 cfz co c1 caddc cstgr cvtx fveq2i stgrvtx eqtrid + eqtri fveq2d hashfz0 eqtrd ) BFGZCHIJBKLZHIBMNLUDCUEHUDCBOIZPIZUECAPIUGEA + UFPDQTBRSUABUBUC $. + + $d G e x $. $d N e n x $. $d V e n x $. + $( All vertices of a star graph S_N except the center are in the (open) + neighborhood of the center. (Contributed by AV, 12-Sep-2025.) $) + stgrnbgr0 $p |- ( N e. NN0 -> ( G NeighbVtx 0 ) = ( V \ { 0 } ) ) $= + ( ve vx vn wcel cc0 co cv wa cedg cfv wrex cdif wceq cpr cvtx cn0 wel csn + cnbgr crab stgrvtx0 eqid dfnbgr2 syl eleq2 anbi12d cfz wss 0elfz fz1ssfz0 + adantr cstgr fveq2i stgrvtx eqtrid difeq1d fz0dif1 eqimssd eqsstrd sselda + c1 eqtri sselid prssd preq2 eqeq2d eqidd rspcedvdw wb stgredgel mpbir2and + weq eleq2i bitrid prid2g adantl c0ex prid1 jctil rabeqcda eqtrd ) BUAIZAJ + UDKZJFLZIZGFUBZMZFANOZPZGCJUCZQZUEZWPWGJCIWHWQRABCDEUFFGWMAJCEWMUGUHUIWGW + NGWPWGGLZWPIZMZWLJJWRSZIZWRXAIZMFXAWMWIXARWJXBWKXCWIXAJUJWIXAWRUJUKWTXAWM + IZXAJBULKZUMZXAJHLZSZRZHVFBULKZPZWTJWRXEWGJXEIWSBUNUPWTXJXEWRBUOWGWPXJWRW + GWPXEWOQZXJWGCXEWOWGCBUQOZTOZXECATOXNEAXMTDURVGBUSUTVAWGXLXJBVBVCVDVEZVHV + IWTXIXAXARHWRXJHGVQXHXAXAXGWRJVJVKXOWTXAVLVMXDXAXMNOZIZWTXFXKMZWMXPXAAXMN + DURVRWGXQXRVNWSHXABVOUPVSVPWTXCXBWSXCWGJWRWPVTWAJWRWBWCWDVMWEWF $. + + $( All vertices of a star graph S_N are in the closed neighborhood of the + center. (Contributed by AV, 12-Sep-2025.) $) + stgrclnbgr0 $p |- ( N e. NN0 -> ( G ClNeighbVtx 0 ) = V ) $= + ( cn0 wcel cc0 cclnbgr co csn cnbgr cun cdif stgrvtx0 dfclnbgr4 stgrnbgr0 + wceq syl uneq2d wss snssd undif sylib 3eqtrd ) BFGZAHIJZHKZAHLJZMZUHCUHNZ + MZCUFHCGUGUJRABCDEOZAHCEPSUFUIUKUHABCDEQTUFUHCUAULCRUFHCUMUBUHCUCUDUE $. + $} + + ${ + isubgr3stgr.v $e |- V = ( Vtx ` G ) $. + isubgr3stgr.u $e |- U = ( G NeighbVtx X ) $. + isubgr3stgr.c $e |- C = ( G ClNeighbVtx X ) $. + ${ + isubgr3stgr.f $e |- F = ( H u. { <. X , Y >. } ) $. + $( Lemma 1 for ~ isubgr3stgr . (Contributed by AV, 16-Sep-2025.) $) + isubgr3stgrlem1 $p |- ( ( H : U -1-1-onto-> R /\ X e. V + /\ ( Y e. W /\ Y e/ R ) ) + -> F : C -1-1-onto-> ( R u. { Y } ) ) $= + ( wf1o wcel wnel wa csn cun w3a cnbgr co wceq wb f1oeq2 biimpi 3ad2ant1 + ax-mp anim2i 3adant1 nbgrnself2 a1i f1ounsn syl112anc cclnbgr dfclnbgr4 + simpl simp3r 3ad2ant2 uncom eqtrdi eqtrid f1oeq2d mpbird ) CBFOZIGPZJHP + ZJBQZRZUAZABJSTZDOEIUBUCZISZTZVLDOZVKVMBFOZVGVHRZIVMQZVIVPVFVGVQVJVFVQC + VMUDVFVQUELCVMBFUFUIUGUHVGVJVRVFVJVHVGVHVIURUJUKVSVKEIULUMVFVGVHVIUSVMB + DFGHIJNUNUOVKAVOVLDVKAEIUPUCZVOMVKVTVNVMTZVOVGVFVTWAUDVJEIGKUQUTVNVMVAV + BVCVDVE $. + $} + + $d U f $. $d W f $. + isubgr3stgr.n $e |- N e. NN0 $. + isubgr3stgr.s $e |- S = ( StarGr ` N ) $. + isubgr3stgr.w $e |- W = ( Vtx ` S ) $. + $( Lemma 2 for ~ isubgr3stgr . (Contributed by AV, 16-Sep-2025.) $) + isubgr3stgrlem2 $p |- ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) + -> E. f f : U -1-1-onto-> ( W \ { 0 } ) ) $= + ( c1 wceq wcel cn0 cvv chash cfv caddc co cusgr w3a cc0 csn cdif wf1o wex + cv stgrorder ax-mp wa cmin oveq1 cc nn0cn pncan1 syl mp1i eqtrd peano2nn0 + adantr cfn eleq1 mpbiri wb cvtx hashclb mpbird stgrvtx0 hashdifsn sylancl + fvexi simpr3 3eqtr4rd 3ad2ant3 cnbgr ovexi diffi hasheqf1o syl2an2 mpbid + mpan ) HUAUBZFPUCUDZQZEUERZIGRZCUAUBZFQZUFZCHUGUHZUIZDULUJDUKZFSRZWIMBFHN + OUMUNWIWNUOZWLWPUAUBZQZWQWSWGPUPUDZFWTWLWIXBFQWNWIXBWHPUPUDZFWGWHPUPUQWRX + CFQZWIMWRFURRXDFUSFUTVAVBVCVEWSHVFRZUGHRZWTXBQWSXEWGSRZWIXGWNWIXGWHSRZWRX + HMFVDUNWGWHSVGVHVEHTRXEXGVIWSHBVJOVPHTVKVBVLZWRXFMBFHNOVMUNHUGVNVOWIWJWKW + MVQVRWNCVFRZWIWPVFRZXAWQVIWNXJWLSRZWMWJXLWKWMXLWRMWLFSVGVHVSCTRXJXLVIWNCE + IVTKWACTVKVBVLWSXEXKXIHWOWBVACWPDWCWDWEWF $. + + $d C f g $. $d G f $. $d N f $. $d V f $. $d W g $. $d X f g $. + $( Lemma 3 for ~ isubgr3stgr . (Contributed by AV, 17-Sep-2025.) $) + isubgr3stgrlem3 $p |- ( ( G e. USGraph /\ X e. V /\ ( # ` U ) = N ) + -> E. g ( g : C -1-1-onto-> W /\ ( g ` X ) = 0 ) ) $= + ( vf wcel wceq cc0 cvv cusgr cfv w3a csn cdif cv wf1o wex isubgr3stgrlem2 + chash wa cdm f1odm cun cop wi wnel simpr simpl2 c0ex a1i neldifsnd df-nel + wn sylibr eqid isubgr3stgrlem1 syl112anc ex wf f1of 3ad2ant2 cclnbgr fexd + ovexi wss stgrvtx0 snssd undifr sylib f1oeq3d biimpa 3adant3 simp12 cnbgr + cn0 mp1i co nbgrnself2 eleq2i xchbinxr mpbi eleq2 notbid 3ad2ant3 fsnunfv + wb mpbiri syl3anc jca f1oeq1 eqeq1d anbi12d spcedv 3exp syld mpdi exlimdv + fveq1 mpd ) EUAQZIGQZCUJUBFRZUCZCHSUDZUEZPUFZUGZPUHAHDUFZUGZIXSUBZSRZUKZD + UHZABCPEFGHIJKLMNOUIXNXRYDPXNXRXQULZCRZYDCXPXQUMXNXRAXPXOUNZXQISUOUDUNZUG + ZYFYDUPXNXRYIXNXRUKZXRXLSTQZSXPUQZYIXNXRURXKXLXMXRUSYKYJUTVAYJSXPQVDYLYJS + HVBSXPVCVEAXPCYHEXQGTISJKLYHVFVGVHVIXNYIYFYDXNYIYFUCZYCAHYHUGZIYHUBZSRZUK + DTYHYMAYGTYHYIXNAYGYHVJYFAYGYHVKVLATQYMAEIVMLVOVAVNYMYNYPXNYIYNYFXNYIYNXN + YGHAYHXNXOHVPYGHRXNSHFWFQSHQXNMBFHNOVQWGVRXOHVSVTWAWBWCYMXLYKIYEQZVDZYPXK + XLXMYIYFWDYKYMUTVAYMYRICQZVDZIEIWEWHZUQZYTEIWIUUBIUUAQYSIUUAVCCUUAIKWJWKW + LYFXNYRYTWQYIYFYQYSYECIWMWNWOWRXQGTISWPWSWTXSYHRZXTYNYBYPAHXSYHXAUUCYAYOS + IXSYHXIXBXCXDXEXFXGXHXJ $. + + $d A z $. $d B a b $. $d B z $. $d C a b $. $d C f g $. $d C z $. + $d F a b $. $d F z $. $d G f $. $d N f $. $d N z $. $d U f $. + $d V f $. $d W f g $. $d W z $. $d X a b $. $d X f g $. $d X z $. + isubgr3stgr.e $e |- E = ( Edg ` G ) $. + $( Lemma 4 for ~ isubgr3stgr . (Contributed by AV, 24-Sep-2025.) $) + isubgr3stgrlem4 $p |- ( ( A = X /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) + /\ ( A =/= B /\ A e. C /\ B e. C ) ) + -> E. z e. ( 1 ... N ) ( F " { A , B } ) = { 0 , z } ) $= + ( va vb wceq wf1o cfv cc0 wa wne wcel w3a cpr cima cv c1 co wrex wi preq2 + cfz eqeq2d wf f1of adantr simpr3 ffvelcdmd wo csn cun cvtx fveq2i stgrvtx + cstgr ax-mp 3eqtri eleq2i fz0sn0fz1 elun fvex elsn orbi1i bitri 3bitri wb + cn0 eqeq2 adantl wf1 f1of1 wral simpl simpr neeq12d fveq2 imbi12d rspc2gv + dff14a 3adant1 id eqneqall eqcoms com12 syl6com 3ad2ant1 adantld biimtrid + syld syl5com imp sylbird idd jaod mpd f1ofn 3simpc anim12i 3anass fnimapr + wfn sylibr syl preq1d eqtrd rspcedvdw neeq1 eleq1 3anbi12d imaeq2d eqeq1d + ex preq1 rexbidv imbitrrid 3imp ) BMUCZDLHUDZMHUEZUFUCZUGZBCUHZBDUIZCDUIZ + UJZHBCUKZULZUFAUMZUKZUCZAUNJUSUOZUPZYRUUBUUIUQYNMCUHZMDUIZUUAUJZHMCUKZULZ + UUFUCZAUUHUPZUQYRUULUUPYRUULUGZUUOUUNUFCHUEZUKZUCAUURUUHUUEUURUCUUFUUSUUN + UUEUURUFURUTUUQUURLUIZUURUUHUIZUUQDLCHYRDLHVAZUULYOUVBYQDLHVBVCVCYRUUJUUK + UUAVDVEUUTUURUFUCZUVAVFZUUQUVAUUTUURUFJUSUOZUIUURUFVGZUUHVHZUIZUVDLUVEUUR + LEVIUEJVLUEZVIUEZUVESEUVIVIRVJJWDUIZUVJUVEUCQJVKVMVNVOUVEUVGUURUVKUVEUVGU + CQJVPVMVOUVHUURUVFUIZUVAVFUVDUURUVFUUHVQUVLUVCUVAUURUFCHVRVSVTWAWBUUQUVCU + VAUVAUUQUVCUURYPUCZUVAYRUVMUVCWCZUULYQUVNYOYPUFUURWEWFVCYRUULUVMUVAUQZYOU + ULUVOUQYQYODLHWGZUULUVODLHWHUVPUVBUAUMZUBUMZUHZUVQHUEZUVRHUEZUHZUQZUBDWIU + ADWIZUGUULUVOUAUBDLHWPUULUWDUVOUVBUULUWDUUJYPUURUHZUQZUVOUUKUUAUWDUWFUQUU + JUWCUWFUAUBMCDDUVQMUCZUVRCUCZUGZUVSUUJUWBUWEUWIUVQMUVRCUWGUWHWJUWGUWHWKWL + UWIUVTYPUWAUURUWGUVTYPUCUWHUVQMHWMVCUWHUWAUURUCUWGUVRCHWMWFWLWNWOWQUUJUUK + UWFUVOUQUUAUWFUUJUWEUVOUWFWRUVMUWEUVAUWEUVAUQYPUURUVAYPUURWSWTXAXBXCXFXDX + EXGVCXHXIUUQUVAXJXKXEXLUUQUUNYPUURUKZUUSUUQHDXRZUUKUUAUJZUUNUWJUCUUQUWKUU + KUUAUGZUGUWLYRUWKUULUWMYOUWKYQDLHXMVCUUJUUKUUAXNXOUWKUUKUUAXPXSDMCHXQXTUU + QYPUFUURYRYQUULYOYQWKVCYAYBYCYIYNUUBUULUUIUUPYNYSUUJYTUUKUUABMCYDBMDYEYFY + NUUGUUOAUUHYNUUDUUNUUFYNUUCUUMHBMCYJYGYHYKWNYLYM $. + + ${ + $d C i $. $d F i $. $d I i $. $d W i $. $d Y i $. + isubgr3stgr.i $e |- I = ( Edg ` ( G ISubGr C ) ) $. + isubgr3stgr.h $e |- H = ( i e. I |-> ( F " i ) ) $. + $( Lemma 5 for ~ isubgr3stgr . (Contributed by AV, 24-Sep-2025.) $) + isubgr3stgrlem5 $p |- ( ( F : C --> W /\ Y e. I ) + -> ( H ` Y ) = ( F " Y ) ) $= + ( wf wcel wa cv cima cvv cmpt wceq imaeq2 adantl simpr id cclnbgr ovexi + a1i fexd adantr imaexd fvmptd ) ALFUDZNIUEZUFZDNFDUGZUHZFNUHZIHUIHDIVGU + JUKVEUCURVFNUKVGVHUKVEVFNFULUMVCVDUNVEFNUIVCFUIUEVDVCALUIFVCUOAUIUEVCAG + MUPQUQURUSUTVAVB $. + + $d C a b i z $. $d E a b i x y $. $d F e z $. $d G a b i $. + $d N a b i $. $d N e i $. $d U a b i x y $. $d V a b i $. $d W a b $. + $d X a b i $. + $( Lemma 6 for ~ isubgr3stgr . (Contributed by AV, 24-Sep-2025.) $) + isubgr3stgrlem6 $p |- ( ( ( ( G e. USGraph /\ X e. V ) + /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) + /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) + -> H : I --> ( Edg ` ( StarGr ` N ) ) ) $= + ( vz va vb cusgr wcel wa chash cfv wceq cv cpr wnel wral wf1o cc0 cstgr + cima cedg wss cuhgr usgruhgr adantr cclnbgr clnbgrssvtx eqsstri cisubgr + wb co a1i eqid isubgredg syl2an cfz c1 wrex wf f1of cvtx fveq2i stgrvtx + cn0 ax-mp 3eqtri eqimssi fssd ad2antrl fimassd simplll simpl usgredg wi + wne vex prss w3a elclnbgrelnbgr expcom eleq2i 3imtr4g im2anan9r 3adant3 + cnbgr imp preq1 eqidd neleq12d preq2 rspc2v syl pm2.24nel 3ad2ant3 syld + adantl 3exp com24 adantld adantrd imp4c simpllr simplrl simprrr simprrl + necomd isubgr3stgrlem4 syl113anc prcom imaeq2i eqeq1i rexbii pm2.61iine + sylibr ex biimtrrid exp32 com23 imbi12d sseq1 eleq1 imaeq2 eqeq1d imp32 + rexbidv mpbird a1d rexlimdvv mpd stgredgel sylanbrc sylbida fmptd ) IUH + UIZOMUIZUJZEUKULLUMZAUNZBUNZUOZGUPZBEUQAEUQZUJZUJZCNHURZOHULUSUMZUJZUJZ + FKHFUNZVAZLUTULZVBULZJUVIUVJKUIZUVJGUIZUVJCVCZUJZUVKUVMUIZUVEIVDUIZCMVC + ZUVNUVQVKUVHUUQUVSUVDUUOUVSUUPIVEVFVFUVTUVHCIOVGVLZMRIOMPVHVIVMCGIICVJV + LZKUVJMPUBUWBVNUCVOVPUVIUVQUJZUVKUSLVQVLZVCZUVKUSUEUNUOZUMZUEVRLVQVLZVS + ZUVRUWCCUWDHUVJUVICUWDHVTZUVQUVFUWJUVEUVGUVFCNUWDHCNHWANUWDVCUVFNUWDNDW + BULUVLWBULZUWDUADUVLWBTWCLWEUIZUWKUWDUMSLWDWFWGWHVMWIWJVFWKUWCUFUNZUGUN + ZWPZUVJUWMUWNUOZUMZUJZUGMVSUFMVSZUWIUVIUUOUVOUWSUVQUUOUUPUVDUVHWLUVOUVP + WMUVJGIMUFUGPUBWNVPUWCUWRUWIUFUGMMUWCUWRUWIWOZUWMMUIUWNMUIUJUVIUVOUVPUW + TUVIUWRUVPUVOUWIUVIUWRUVPUVOUWIWOZWOZUVIUWRUJZUXBUWPCVCZUWPGUIZHUWPVAZU + WFUMZUEUWHVSZWOZWOZUXCUXEUXDUXHUVIUWRUXEUXDUXHWOZWOZUVIUWOUXLUWQUVIUWOU + XEUXKUXDUWMCUIZUWNCUIZUJZUVIUWOUXEUJZUJZUXHUWMUWNCUFWQUGWQWRUXQUXOUXHUX + QUXOUJZUXHWOUWNUWMOOUWNOWPZUWMOWPZUJZUVIUXPUXOUXHUYAUVEUXPUXOUXHWOWOZUV + HUYAUVDUYBUUQUYAUVCUYBUURUYAUXOUXPUVCUXHUYAUXOUXPUVCUXHWOUYAUXOUXPWSZUV + CUWPGUPZUXHUYCUWMEUIZUWNEUIZUJZUVCUYDWOUYAUXOUYGUXPUYAUXOUYGUXTUXMUYEUX + SUXNUYFUXTUWMUWAUIZUWMIOXFVLZUIZUXMUYEUYHUXTUYJIOUWMWTXACUWAUWMRXBEUYIU + WMQXBXCUXSUWNUWAUIZUWNUYIUIZUXNUYFUYKUXSUYLIOUWNWTXACUWAUWNRXBEUYIUWNQX + BXCXDXGXEUVBUYDUWMUUTUOZGUPABUWMUWNEEUUSUWMUMZUVAUYMGGUUSUWMUUTXHUYNGXI + XJUUTUWNUMZUYMUWPGGUUTUWNUWMXKUYOGXIXJXLXMUXPUYAUYDUXHWOZUXOUXEUYPUWOUX + HUWPGXNXQXOXPXRXSXTXTYAYBUWNOUMZUXRUXHUYQUXRUJZHUWNUWMUOZVAZUWFUMZUEUWH + VSZUXHUYRUYQUVHUWNUWMWPZUXNUXMVUBUYQUXRWMUXRUVHUYQUVEUVHUXPUXOYCZXQUXRV + UCUYQUXRUWMUWNUVIUWOUXEUXOYDZYGXQUYQUXQUXMUXNYEUYQUXQUXMUXNYFUEUWNUWMCD + EGHILMNOPQRSTUAUBYHYIUXGVUAUEUWHUXFUYTUWFUWPUYSHUWMUWNYJYKYLYMYOYPUWMOU + MZUXRUXHVUFUXRUJVUFUVHUWOUXMUXNUXHVUFUXRWMUXRUVHVUFVUDXQUXRUWOVUFVUEXQV + UFUXQUXMUXNYFVUFUXQUXMUXNYEUEUWMUWNCDEGHILMNOPQRSTUAUBYHYIYPYNYPYQYRYAX + GYSUWRUXBUXJVKZUVIUWQVUGUWOUWQUVPUXDUXAUXIUVJUWPCUUAUWQUVOUXEUWIUXHUVJU + WPGUUBUWQUWGUXGUEUWHUWQUVKUXFUWFUVJUWPHUUCUUDUUFYTYTXQXQUUGYPXSUUEUUHUU + IUUJUWLUVRUWEUWIUJVKSUEUVKLUUKWFUULUUMUDUUN $. + + $d C y $. $d F y $. $d G y $. $d I y $. $d J y $. $d N y $. + $d V y $. $d W y $. $d X y $. + $( Lemma 7 for ~ isubgr3stgr . (Contributed by AV, 29-Sep-2025.) $) + isubgr3stgrlem7 $p |- ( ( ( G e. USGraph /\ X e. V ) + /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) + /\ J e. ( Edg ` ( StarGr ` N ) ) ) + -> ( `' F " J ) e. I ) $= + ( vy cusgr wcel wa wf1o cfv cc0 wceq cstgr cedg ccnv cima cfz co wss cv + cpr c1 wrex cn0 wb stgredgel mp1i wi wfn w3a cvv a1i prssg sylan f1ocnv + c0ex f1ofn fveq2i stgrvtx ax-mp 3eqtri fneq2i sylib syl ad2antrl adantr + cvtx anim1i 3anass sylibr ex sylbird fnimapr cclnbgr clnbgrvtxel adantl + imp eleqtrrdi simpl anim12ci simprr jca f1ocnvfv ad3antlr f1of fz1ssfz0 + wf sseli ffvelcdmd wo eleq2i cupgr usgrupgr ad2antrr clnbgrssvtx sselid + eqsstri df-3an sylanbrc clnbupgrel eqeq2 wf1 f1of1 0elfz eleqtrri jctir + bitrid f1veqaeq syl2an cn elfznn wne nnne0 eqneqall syl5com syld eleq1i + prcom sylbid eleq1d mpbird biimpi jaod impr prssi mpidan sseq1d anbi12d + preq1 mpdan cuhgr ad3antrrr cisubgr eqid isubgredg eqeltrd sseq1 imaeq2 + usgruhgr imbi12d syl5ibrcom rexlimdva impcomd 3impia ) GUEUFZNLUFZUGZAM + FUHZNFUIUJUKZUGZJKULUIZUMUIUFZFUNZJUOZIUFZUVFUVIUGZUVKJUJKUPUQZURZJUJUD + USZUTZUKZUDVAKUPUQZVBZUGZUVNKVCUFZUVKUWCVDUVORUDJKVEVFUVOUWBUVQUVNUVOUV + TUVQUVNVGZUDUWAUVOUVRUWAUFZUGZUWEUVTUVSUVPURZUVLUVSUOZIUFZVGUWGUWHUWJUW + GUWHUGZUWIUJUVLUIZUVRUVLUIZUTZIUWKUVLUVPVHZUJUVPUFZUVRUVPUFZVIZUWIUWNUK + UWGUWHUWRUWGUWHUWPUWQUGZUWRUVOUJVJUFZUWFUWSUWHVDUWTUVOVOVKUJUVRUVPVJUWA + VLVMUWGUWSUWRUWGUWSUGUWOUWSUGUWRUWGUWOUWSUVOUWOUWFUVGUWOUVFUVHUVGMAUVLU + HZUWOAMFVNZUXAUVLMVHUWOMAUVLVPMUVPUVLMBWFUIUVJWFUIZUVPTBUVJWFSVQUWDUXCU + VPUKRKVRVSVTZWAWBWCWDWEWGUWOUWPUWQWHWIWJWKWPUVPUJUVRUVLWLWCUWKUWNIUFZUW + NEUFZUWNAURZUGZUWGUXHUWHUWGUWLNUKZUXHUWGUVGNAUFZUGZUVHUGZUXIUVOUXLUWFUV + OUXKUVHUVFUXJUVIUVGUVFNGNWMUQZAUVENUXMUFUVDGNLOWNZWOQWQUVGUVHWRWSUVFUVG + UVHWTXAWEUXKUVHUXIAMNUJFXBWPWCUWGUXIUGZUXHNUWMUTZEUFZUXPAURZUGZUWGUXIUX + JUWMAUFZUGZUXSUWGUXJUXTUVEUXJUVDUVIUWFUVENUXMAUXNQWQXCUWGMAUVRUVLUVOMAU + VLXFZUWFUVGUYBUVFUVHUVGUXAUYBUXBMAUVLXDWCWDWEUWFUVRMUFZUVOUWFUVRUVPMUWA + UVPUVRKXEXGUXDWQZWOXHZXAUXOUYAUGUXQUXRUXOUXJUXTUXQUXOUXJUGZUXTUWMNUKZUW + MNUTZEUFZXIZUXQUXTUWMUXMUFZUYFUYJAUXMUWMQXJUYFGXKUFZUVEUWMLUFZVIZUYKUYJ + VDUWGUYNUXIUXJUWGUYLUVEUGZUYMUYNUVFUYOUVIUWFUVDUYLUVEGXLWGXMUWGALUWMAUX + MLQGNLOXNXPZUYEXOUYLUVEUYMXQXRXMEGNUWMLOUAXSWCYFUYFUYGUXQUYIUXOUYGUXQVG + UXJUXOUYGUWMUWLUKZUXQUXIUYQUYGVDUWGUWLNUWMXTWOUWGUYQUXQVGUXIUWGUYQUVRUJ + UKZUXQUVOMAUVLYAZUYCUJMUFZUGUYQUYRVGUWFUVGUYSUVFUVHUVGUXAUYSUXBMAUVLYBW + CWDUWFUYCUYTUYDUJUVPMUWDUWPRKYCVSUXDYDYEMAUVRUJUVLYGYHUWFUYRUXQVGZUVOUW + FUVRYIUFZVUAUVRKYJVUBUVRUJYKUYRUXQUVRYLUXQUVRUJYMYNWCWOYOWEWKWEUYIUXQVG + UYFUYIUXQUYHUXPEUWMNYQYPUUAVKUUBYRUUCUYAUXRUXONUWMAUUDWOXAUUEUXIUXHUXSV + DUWGUXIUXFUXQUXGUXRUXIUWNUXPEUWLNUWMUUHZYSUXIUWNUXPAVUCUUFUUGWOYTUUIWEU + WGGUUJUFZALURZUXEUXHVDUWHUVDVUDUVEUVIUWFGUURUUKVUEUWHUYPVKAEGGAUULUQZIU + WNLOUAVUFUUMUBUUNYHYTUUOWJUVTUVQUWHUVNUWJJUVSUVPUUPUVTUVMUWIIJUVSUVLUUQ + YSUUSUUTUVAUVBYRUVC $. + + $d C i j k y $. $d E j k $. $d F j k $. $d G j k $. $d I j k $. + $d N j k $. $d U j k x $. $d V j k $. $d W j k $. $d X j k $. + $( Lemma 8 for ~ isubgr3stgr . (Contributed by AV, 29-Sep-2025.) $) + isubgr3stgrlem8 $p |- ( ( ( ( G e. USGraph /\ X e. V ) + /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) + /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) + -> H : I -1-1-onto-> ( Edg ` ( StarGr ` N ) ) ) $= + ( vk vj cusgr wcel wa chash cfv wceq cpr wnel wral wf1o cstgr cedg cima + cv cc0 ccnv cmpt imaeq2 cbvmptv eqtri wf ad2antrl isubgr3stgrlem5 sylan + isubgr3stgrlem6 ffvelcdmda eqeltrrd isubgr3stgrlem7 ad4ant134 wfo f1ofo + f1of wss stgrusgra mp1i simpr c2 cvtx fveq2i eqid edgssv2 simpld syl2an + cn0 foimacnv syl2an2r eqcomd sylan9req f1of1 wi cuhgr usgruhgr ad2antrr + wf1 wb cclnbgr clnbgrssvtx eqsstri a1i cisubgr isubgredg biimtrdi imp32 + co a1d f1imacnv sylan9eqr impbida f1o2d ) IUGUHZOMUHZUIZEUJUKLULAUTBUTU + MGUNBEUOAEUOUIZUIZCNHUPZOHUKVAULZUIZUIZUEUFKLUQUKZURUKZHUEUTZUSZHVBZUFU + TZUSZJJFKHFUTZUSZVCUEKYHVCUDFUEKYMYHYLYGHVDVEVFYDYGKUHZUIYGJUKZYHYFYDCN + HVGZYNYOYHULYAYPXTYBCNHVRVHCDEFGHIJKLMNOYGPQRSTUAUBUCUDVIVJYDKYFYGJABCD + EFGHIJKLMNOPQRSTUAUBUCUDVKVLVMXRYCYJYFUHZYKKUHXSCDEFGHIJKYJLMNOPQRSTUAU + BUCUDVNVOYDYNYQUIZUIZYGYKULZYJYHULZYSYTYJHYKUSZYHYDCNHVPZYRYJNVSZUUBYJU + LYAUUCXTYBCNHVQVHYDYEUGUHZYQUUDYRLWJUHUUEYDSLVTWAYNYQWBUUEYQUIUUDYJUJUK + WCULYJYFYENNDWDUKYEWDUKUADYEWDTWEVFYFWFWGWHWICNYJHWKWLYTYHUUBYGYKHVDWMW + NYSUUAUIYKYGUUAYSYKYIYHUSZYGYJYHYIVDYDCNHWTZYRYGCVSZUUFYGULYAUUGXTYBCNH + WOVHYDYNYQUUHYDYNYGIURUKZUHZUUHUIZYQUUHWPXTIWQUHZCMVSZYNUUKXAYCXPUULXQX + SIWRWSUUMYCCIOXBXJMRIOMPXCXDXECUUIIICXFXJZKYGMPUUIWFUUNWFUCXGWIUUKUUHYQ + UUJUUHWBXKXHXICNYGHXLWLXMWMXNXO $. + + $d C e $. $d E e $. $d G e $. $d U e x y $. $d V e $. $d W e $. + $d X e $. + $( Lemma 9 for ~ isubgr3stgr . (Contributed by AV, 29-Sep-2025.) $) + isubgr3stgrlem9 $p |- ( ( ( ( G e. USGraph /\ X e. V ) + /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) + /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) + -> ( H : I -1-1-onto-> ( Edg ` ( StarGr ` N ) ) + /\ A. e e. I ( F " e ) = ( H ` e ) ) ) $= + ( cusgr wcel wa chash cfv wceq cpr wnel wral wf1o cstgr isubgr3stgrlem8 + cv cc0 cedg cima wf ad2antrl isubgr3stgrlem5 eqcomd sylan ralrimiva jca + f1of ) JUFUGPNUGUHEUIUJMUKAURBURULHUMBEUNAEUNUHUHZCOIUOZPIUJUSUKZUHUHZL + MUPUJUTUJKUOIFURZVAZVNKUJZUKZFLUNABCDEGHIJKLMNOPQRSTUAUBUCUDUEUQVMVQFLV + MCOIVBZVNLUGZVQVKVRVJVLCOIVIVCVRVSUHVPVOCDEGHIJKLMNOPVNQRSTUAUBUCUDUEVD + VEVFVGVH $. + $} + + $d C e i y $. $d E e f i x y $. $d G e g i y $. $d N e f g i x y $. + $d U e i x y $. $d V e i y $. $d W e i y $. $d X e i y $. + $( 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. (Contributed by AV, 29-Sep-2025.) $) + isubgr3stgr $p |- ( ( G e. USGraph /\ X e. V ) + -> ( ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) + -> ( G ISubGr C ) ~=gr ( StarGr ` N ) ) ) $= + ( wcel cfv vf vg ve vi cusgr wa chash wceq cv cpr wnel wral cisubgr cstgr + co cgric wbr cvtx wf1o cedg wex cc0 simpl simpr isubgr3stgrlem3 syl2an3an + cima wss cclnbgr clnbgrssvtx eqsstri a1i anim2i adantr syl eqcomd f1oeq2d + isubgrvtx biimpd adantrd imp cmpt cvv fvexd mptexd isubgr3stgrlem9 f1oeq1 + eqid fveq1 eqeq2d ralbidv anbi12d spcedv jca eximdv mpd cushgr isubgrusgr + ex cuspgr usgruspgr uspgrushgr cn0 stgrusgra ax-mp fveq2i eqtri gricushgr + wb 3syl sylancl mpbird ) GUESZKISZUFZEUGTHUHZAUIBUIUJFUKBEULAEULZUFZGCUMU + OZHUNTZUPUQZXOXRUFZYAXSURTZJUAUIZUSZXSUTTZXTUTTZUBUIZUSZYDUCUIZVGZYJYHTZU + HZUCYFULZUFZUBVAZUFZUAVAZYBCJYDUSZKYDTVBUHZUFZUAVAZYRXOXMXNXRXPUUBXMXNVCX + MXNVDXPXQVCCDEUAGHIJKLMNOPQVEVFYBUUAYQUAYBUUAYQYBUUAUFZYEYPYBUUAYEYBYSYEY + TYBYSYEYBCYCJYDYBYCCYBXMCIVHZUFZYCCUHXOUUEXRXNUUDXMUUDXNCGKVIUOINGKILVJVK + VLVMZVNCGIUELVRVOVPVQVSVTWAUUCYOYFYGUDYFYDUDUIVGZWBZUSZYKYJUUHTZUHZUCYFUL + ZUFUBWCUUHUUCUDYFUUGWCUUCXSUTWDWEABCDEUCUDFYDGUUHYFHIJKLMNOPQRYFWHZUUHWHW + FYHUUHUHZYIUUIYNUULYFYGYHUUHWGUUNYMUUKUCYFUUNYLUUJYKYJYHUUHWIWJWKWLWMWNWS + WOWPXOYAYRXIZXRXOXSWQSZXTWQSZUUOXOXSUESZXSWTSUUPXOUUEUURUUFCGILWRVOXSXAXS + XBXJHXCSZUUQOUUSXTUESXTWTSUUQHXDXTXAXTXBXJXEXSXTUCUAUBYFYGYCJYCWHJDURTXTU + RTQDXTURPXFXGUUMYGWHXHXKVNXLWS $. + $} + + $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- Local isomorphisms of graphs @@ -820759,6 +821352,35 @@ two graphs which are not (ordinary) isomorphisms between these graphs, as UKURTUQABUAKGUMUQABUBABUQUCUDUEUFUGRRUH $. $} + ${ + $d G f x y $. $d H f x y $. $d N f x y $. $d V f x $. $d W f x y $. + clnbgr3stgrgrlic.n $e |- N e. NN0 $. + clnbgr3stgrgrlic.v $e |- V = ( Vtx ` G ) $. + clnbgr3stgrgrlic.w $e |- W = ( Vtx ` H ) $. + $( 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. (Contributed by AV, + 29-Sep-2025.) $) + clnbgr3stgrgrlic $p |- ( ( ( G e. USGraph /\ H e. USGraph /\ V ~~ W ) + /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( StarGr ` N ) + /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) + -> G ~=lgr H ) $= + ( vf cusgr wcel wbr w3a cclnbgr co cgric wa wi cen cisubgr cstgr cfv wral + cv cgrlic wf1o wex cvv wb cvtx fvexi pm3.2i breng mp1i cuhgr wss usgruhgr + adantl 3ad2ant1 clnbgrssvtx a1i isubgruhgr syl2an2r wf 3ad2ant2 ffvelcdmd + f1of simp3 wceq oveq2 oveq2d breq1d rspcv syl com34 3imp1 gricsym anim1ci + 3exp sylc grictr ex ralimdva com24 imp32 ancld eximdv com23 sylbid 3impia + 3impib dfgrlic2 3adant3 mpbird ) CLMZDLMZFGUANZOZCCAUFZPQUBQZEUCUDZRNZAFU + EZDDBUFZPQZUBQZXCRNZBGUEZOCDUGNZFGKUFZUHZXBDDXAXLUDZPQZUBQZRNZAFUEZSZKUIZ + WTXEXJXTWQWRWSXEXJSZXTTZWQWRSZWSXMKUIZYBFUJMZGUJMZSWSYDUKYCYEYFFCULIUMGDU + LJUMUNFGKUJUJUOUPYCYAYDXTYCYAYDXTTYCYASZXMXSKYGXMXRYCXEXJXMXRTYCXMXJXEXRY + CXMXJXEXRTYCXMXJOZXDXQAFYHXAFMZSZXDXQYJXDSXDXCXPRNZSXQYJYKXDYJXPUQMZXPXCR + NZYKYHDUQMZYIXOGURZYLYCXMYNXJWRYNWQDUSUTVAYOYJDXNGJVBVCXODGJVDVEYCXMXJYIY + MYCXMYIXJYMYCXMYIXJYMTZYCXMYIOZXNGMYPYQFGXAXLXMYCFGXLVFYIFGXLVIVGYCXMYIVJ + VHXIYMBXNGXFXNVKZXHXPXCRYRXGXODUBXFXNDPVLVMVNVOVPWAVQVRXCXPVSWBVTXBXCXPWC + VPWDWEWAWFWGWHWIWDWJWKWLWMWTXEXKXTUKZXJWQWRYSWSAKCDFGLLIJWNWOVAWP $. + $} + ${ $d V e $. usgrexmpl1.v $e |- V = ( 0 ... 5 ) $. @@ -821650,6 +822272,29 @@ definition is not meaningful (since then ` ( |^ `` ( n / 2 ) ) <_ 1 ` BXHXIVNVJVOVPVQVRWGVSGWHWOVTWFBALWACVSWIWGWLWLTWITWBVBVR $. $} + ${ + gpgorder.j $e |- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) ) $. + $( The order of the generalized Petersen graph GPG(N,K). (Contributed by + AV, 29-Sep-2025.) $) + gpgorder $p |- ( ( N e. NN /\ K e. J ) + -> ( # ` ( Vtx ` ( N gPetersenGr K ) ) ) = ( 2 x. N ) ) $= + ( cn wcel wa cgpg co cvtx cfv chash cc0 c1 cpr cfzo cmul c2 cfn wceq eqid + cxp gpgvtx fveq2d prfi fzofi pm3.2i mp1i prhash2ex a1i cn0 nnnn0 hashfzo0 + hashxp syl adantr oveq12d 3eqtrd ) CEFZBAFZGZCBHIJKZLKMNOZMCPIZUBZLKZVCLK + ZVDLKZQIZRCQIVAVBVELVDABCDVDUAUCUDVCSFZVDSFZGVFVITVAVJVKMNUEMCUFUGVCVDUNU + HVAVGRVHCQVGRTVAUIUJUSVHCTZUTUSCUKFVLCULCUMUOUPUQUR $. + $} + + $( The order of a generalized Petersen graph G(5,K), which is either the + Petersen graph G(5,2) or the 5-prism G(5,1), is 10. (Contributed by AV, + 26-Aug-2025.) $) + gpg5order $p |- ( K e. ( 1 ... 2 ) + -> ( # ` ( Vtx ` ( 5 gPetersenGr K ) ) ) = ; 1 0 ) $= + ( c1 c2 cfz co wcel c5 cgpg cvtx cfv chash cmul cc0 cn cdiv cceil cfzo wceq + cdc 5nn caddc cz 2z fzval3 ax-mp c3 2p1e3 eqtr4i oveq2i eqtri eleq2i biimpi + ceil5half3 eqid gpgorder sylancr 5cn 2cn 5t2e10 mulcomli eqtrdi ) ABCDEZFZG + AHEIJKJZCGLEZBMSZVCGNFABGCOEPJZQEZFZVDVERTVCVIVBVHAVBBCBUAEZQEZVHCUBFVBVKRU + CBCUDUEVJVGBQVJUFVGUGUMUHUIUJUKULVHAGVHUNUOUPGCVFUQURUSUTVA $. $( The ceiling of half of an integer greater than 2 is greater than or equal to 2. (Contributed by AV, 4-Sep-2025.) $) @@ -822384,8 +823029,8 @@ connected by an edge (i.e., the (closed) neighborhood of every vertex for every generalized Petersen graph: for example, in the 3-prism G(3,1) (see gpg31grim3prism TODO) and the Dürer graph G(6,2) there are vertices which have neighborhoods containing triangles. In general, all - generalized Peterson graphs G(N,K) with ` N = 3 x. K ` contain - triangles. (Contributed by AV, 8-Sep-2025.) $) + generalized Petersen graphs G(N,K) with ` N = 3 x. K ` contain triangles + (see gpg3kgrtriex TODO). (Contributed by AV, 8-Sep-2025.) $) gpg5nbgr3star $p |- ( ( N = 5 /\ K e. J /\ X e. V ) -> ( ( # ` U ) = 3 /\ A. x e. U A. y e. U { x , y } e/ E ) ) $= ( wceq wcel wb syl neleq1 va vb c5 w3a cv cop cc0 cfzo co wrex c1 cpr cfv @@ -822451,6 +823096,48 @@ generalized Peterson graphs G(N,K) with ` N = 3 x. K ` contain BVKCGUHUIUPUJCDUKULUMVBVCVDUNVIVDTVHVFFAEIUOUQURVGABCDEFGHIVGUSUTVA $. $} + ${ + $d G x y $. $d K x y $. $d V x y $. + gpg5gricstgr3.g $e |- G = ( 5 gPetersenGr K ) $. + $( Each closed neighborhood in a generalized Petersen graph G(N,K) of order + 10 ( ` N = 5 ` ), which is either the Petersen graph G(5,2) or the + 5-prism G(5,1), is isomorphic to a 3-star. (Contributed by AV, + 13-Sep-2025.) $) + gpg5gricstgr3 $p |- ( ( K e. ( 1 ... 2 ) /\ V e. ( Vtx ` G ) ) + -> ( G ISubGr ( G ClNeighbVtx V ) ) ~=gr ( StarGr ` 3 ) ) $= + ( vx vy c1 c2 co wcel cvtx cfv wa cusgr c3 wceq cv c5 cfzo eqid cfz cnbgr + chash cpr cedg wnel wral cclnbgr cisubgr cstgr cgric wbr cuz cceil 5eluz3 + caddc cz fzval3 ax-mp 2p1e3 oveq2i ceil5half3 eqcomi 3eqtri eleq2i biimpi + cdiv 2z gpgusgra eqeltrid sylancr anim1i eqidd adantr simpr gpg5nbgr3star + cgpg syl3anc 3nn0 isubgr3stgr sylc ) BGHUAIZJZCAKLZJZMZANJZWEMACUBIZUCLOP + EQFQUDAUELZUFFWHUGEWHUGMZAACUHIZUIIOUJLZUKULWCWGWEWCROUMLJZBGRHVGIUNLZSIZ + JZWGUOWCWPWBWOBWBGHGUPIZSIZGOSIWOHUQJWBWRPVHGHURUSWQOGSUTVAOWNGSWNOVBVCVA + VDVEVFZWMWPMARBVQINDBRVIVJVKVLWFRRPWPWEWJWFRVMWCWPWEWSVNWCWEVOEFWHWIAWOBR + WDCWOTDWDTZWHTZWITZVPVREFWKWLWHWIAOWDWLKLZCWTXAWKTVSWLTXCTXBVTWA $. + $} + + ${ + $d v w $. + $( 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. (Contributed by AV, 29-Sep-2025.) $) + gpg5grlic $p |- ( 5 gPetersenGr 1 ) ~=lgr ( 5 gPetersenGr 2 ) $= + ( vv vw c5 c1 cgpg co cusgr wcel c2 cvtx cfv wbr c3 cfzo mp2an wceq ax-mp + cuz cvv eqid cen w3a cclnbgr cisubgr cstgr cgric wral cgrlic cceil 5eluz3 + cv cdiv cz 3z 1lt3 eluz2b1 mpbir2an fzo1lb mpbir ceil5half3 eqcomi oveq2i + clt eleqtri gpgusgra cn 2nn 3nn 2lt3 elfzo1 mpbir3an cc0 cdc cfz 2eluzge1 + chash eluzfz1 gpg5order eluzfz2 wa eqtr3 cfn wb cn0 fvex hashvnfin hashen + 10nn0 syl2an mpbid 3pm3.2i gpg5gricstgr3 mpan rgen clnbgr3stgrgrlic mp3an + wi 3nn0 ) CDEFZGHZCIEFZGHZWSJKZXAJKZUALZUBWSWSAUKZUCFUDFMUEKZUFLZAXCUGXAX + ABUKZUCFUDFXGUFLZBXDUGWSXAUHLWTXBXECMRKHZDDCIULFUIKZNFZHWTUJDDMNFZXMDXNHM + IRKHZXOMUMHDMVCLUNUOMUPUQMURUSMXLDNXLMUTVAVBZVDDCVEOXKIXMHXBUJIXNXMIXNHIV + FHMVFHIMVCLVGVHVIMIVJVKXPVDICVEOXCVPKZDVLVMZPZXDVPKZXRPZXEDDIVNFZHZXSIDRK + HZYCVODIVQQZDVRQIYBHZYAYDYFVODIVSQZIVRQXSYAVTXQXTPZXEXQXTXRWAXSXCWBHZXDWB + HZYHXEWCYAXCSHXRWDHZXSYIWQWSJWEWHXCXRSWFOXDSHYKYAYJWQXAJWEWHXDXRSWFOXCXDW + GWIWJOWKXHAXCYCXFXCHXHYEWSDXFWSTWLWMWNXJBXDYFXIXDHXJYGXAIXIXATWLWMWNABWSX + AMXCXDWRXCTXDTWOWP $. + $} + $( @{ gpg31grim3prism.v @e |- V = ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) @. @@ -822462,6 +823149,14 @@ generalized Peterson graphs G(N,K) with ` N = 3 x. K ` contain gpg31grim3prism @p |- ( 3 gPetersenGr 1 ) ~=gr <. V , ( _I |` E ) >. @= ? @. @} + + @{ + gpg3kgrtriex.g @e |- G = ( ( 3 x. K ) gPetersenGr K ) @. + @( All generalized Petersen graphs G(N,K) with ` N = 3 x. K ` contain + triangles. (Contributed by AV, 8-Sep-2025.) @) + gpg3kgrtriex @p |- ( K e. NN -> E. t t e. ( GrTriangles ` G ) ) @= + ? @. + @} $)