Graphs being locally isomorphic but not isomorphic (1) (#4969)

* Sections "Triangles in graphs" and "Local isomorphisms of graphs" swapped

* First graph for graphs being locally isomorphic but not isomorphic

* theorems moved from TA's mathbox 8and proofs shortened): ~s2rn, ~s3rn
* new auxiliary theorems in main: ~fz0to5un2tp, ~hash7g, ~s7rn, ~s7f1o
* proofs shortened for ~fz0to4untppr, ~usgrexmpl
* First graph for graphs being locally isomorphic but not isomorphic: basic properties, especially that it contais a triangle (~usgrexmpl1tri)

* Second graph for graphs being locally isomorphic but not isomorphic

* Second graph for graphs being locally isomorphic but not isomorphic: basic properties

* Neighborhoods in the second graph for graphs being locally isomorphic but not isomorphic

* ~bj-biorfi moved from BJ's mathbox to main
* ~eqrrabd moved from TA's mathbox to main
* new theorems ~usgrexmpl2nb in AV's mathbox

* The second graph for graphs being locally isomorphic but not isomorphic is triangle-free.

* ~elv3 moved from PM's mathbox to main
* new theorems ~usgrgrtrirex and ~usgrexmpl2trifr in AV's mathbox

* Theorems for graphs being locally isomorphic but not isomorphic moved...

from sections "Triangles in graphs" into section "Local isomorphisms of graphs"

* Two graphs which are not isomorphic

* ~bj-pm2.01i moved from BJ's mathbox to main
* new theorem ~usgrexmpl12ngric in AV's mathbox

* renamings

* ~bj-pm2.01i renamed ~pm2.01i
* ~biorfi renamed ~biorfri (as proposed by BJ) and proof shortened
* ~bj-biorfi renamed ~biorfi
* 2 proofs using ~biorfri (formerly ~biorfi) shortend by the minimize script

* discouraged, rewarp

* TA's review remarks

* labels of hypotheses for ~usgrgrtrirex adjusted
* ~usgrexmpl2nblem2 generalized to ~el7g (analogous to ~eltpg)

---------

Co-authored-by: Wolf Lammen <[email protected]>
Co-authored-by: tirix <[email protected]>

Author: 3 people

changes-set.txt

@@ -96,7 +96,14 @@ Date      Old       New         Notes
 18-Aug-25 cbvsum    [same]      Removed unneeded hypotheses
 17-Aug-25 bj-denotes iseqsetv-clel Moved from BJ's mathbox to main
 17-Aug-25 bj-issettru issettru  Moved from BJ's mathbox to main set.mm
+10-Aug-25 bj-biorfi biorfi      Moved from BJ's mathbox to main set.mm
+10-Aug-25 biorfi    biorfri
+10-Aug-25 bj-pm2.01i pm2.01i    Moved from BJ's mathbox to main set.mm
+10-Aug-25 eqrrabd   [same]      Moved from TA's mathbox to main set.mm
+10-Aug-25 el3v      [same]      Moved from PM's mathbox to main set.mm
  9-Aug-25 frobrhm   [same]      Moved from TA's mathbox to main set.mm
+ 7-Aug-25 s3rn      [same]      Moved from TA's mathbox to main set.mm
+ 7-Aug-25 s2rn      [same]      Moved from TA's mathbox to main set.mm
 28-Jul-25 spcimgft  spcimgfi1   Is a kind of inference form
 27-Jul-25 fnimatp   fnimatpd    Moved from TA's mathbox to main set.mm
 25-Jul-25 alcomiw   alcomimw    Consistent with excomimw, excomim

discouraged

@@ -14999,6 +14999,7 @@ New usage of "bdopssadj" is discouraged (4 uses).
 New usage of "biadaniALT" is discouraged (0 uses).
 New usage of "bian1dOLD" is discouraged (0 uses).
 New usage of "bicomdALT" is discouraged (0 uses).
+New usage of "biorfriOLD" is discouraged (0 uses).
 New usage of "bitr3VD" is discouraged (0 uses).
 New usage of "bj-0" is discouraged (1 uses).
 New usage of "bj-1" is discouraged (0 uses).
@@ -19172,6 +19173,8 @@ New usage of "ruvALT" is discouraged (0 uses).
 New usage of "rzalALT" is discouraged (0 uses).
 New usage of "s1dmALT" is discouraged (0 uses).
 New usage of "s2dmALT" is discouraged (0 uses).
+New usage of "s2rnOLD" is discouraged (0 uses).
+New usage of "s3rnOLD" is discouraged (0 uses).
 New usage of "sb1" is discouraged (2 uses).
 New usage of "sb10f" is discouraged (0 uses).
 New usage of "sb2" is discouraged (8 uses).
@@ -20080,6 +20083,7 @@ Proof modification of "bhmafibid1" is discouraged (429 steps).
 Proof modification of "biadaniALT" is discouraged (28 steps).
 Proof modification of "bian1dOLD" is discouraged (36 steps).
 Proof modification of "bicomdALT" is discouraged (12 steps).
+Proof modification of "biorfriOLD" is discouraged (16 steps).
 Proof modification of "bitr3VD" is discouraged (36 steps).
 Proof modification of "bj-0" is discouraged (5 steps).
 Proof modification of "bj-1" is discouraged (5 steps).
@@ -20125,7 +20129,6 @@ Proof modification of "bj-axsn" is discouraged (12 steps).
 Proof modification of "bj-axtd" is discouraged (26 steps).
 Proof modification of "bj-bibibi" is discouraged (34 steps).
 Proof modification of "bj-bijust0ALT" is discouraged (6 steps).
-Proof modification of "bj-biorfi" is discouraged (12 steps).
 Proof modification of "bj-brrelex12ALT" is discouraged (66 steps).
 Proof modification of "bj-cbv1hv" is discouraged (62 steps).
 Proof modification of "bj-cbv2hv" is discouraged (67 steps).
@@ -21590,6 +21593,8 @@ Proof modification of "ruvALT" is discouraged (24 steps).
 Proof modification of "rzalALT" is discouraged (21 steps).
 Proof modification of "s1dmALT" is discouraged (25 steps).
 Proof modification of "s2dmALT" is discouraged (38 steps).
+Proof modification of "s2rnOLD" is discouraged (154 steps).
+Proof modification of "s3rnOLD" is discouraged (187 steps).
 Proof modification of "sb56OLD" is discouraged (25 steps).
 Proof modification of "sb5ALT" is discouraged (80 steps).
 Proof modification of "sb5ALTVD" is discouraged (110 steps).