| Metamath
Proof Explorer Theorem List (p. 480 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | clnbgrgrimlem 47901* | Lemma for clnbgrgrim 47902: For two isomorphic hypergraphs, if there is an edge connecting the image of a vertex of the first graph with a vertex of the second graph, the vertex of the second graph is the image of a neighbor of the vertex of the first graph. (Contributed by AV, 2-Jun-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝐸 = (Edg‘𝐻) ⇒ ⊢ (((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊)) → ((𝐾 ∈ 𝐸 ∧ {(𝐹‘𝑋), 𝑌} ⊆ 𝐾) → ∃𝑛 ∈ (𝐺 ClNeighbVtx 𝑋)(𝐹‘𝑛) = 𝑌)) | ||
| Theorem | clnbgrgrim 47902 | Graph isomorphisms between hypergraphs map closed neighborhoods onto closed neighborhoods. (Contributed by AV, 2-Jun-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝐻 ClNeighbVtx (𝐹‘𝑋)) = (𝐹 “ (𝐺 ClNeighbVtx 𝑋))) | ||
| Theorem | grimedg 47903 | Graph isomorphisms map edges onto the corresponding edges. (Contributed by AV, 7-Jun-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (Edg‘𝐺) & ⊢ 𝐸 = (Edg‘𝐻) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → (𝐾 ∈ 𝐼 ↔ ((𝐹 “ 𝐾) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉))) | ||
Usually, a "triangle" in graph theory is a complete graph consisting of three vertices (denoted by " K3 "), see the definition in [Diestel] p. 3 or the definition in [Bollobas] p. 5. This corresponds to the definition of a "triangle graph" (which is a more precise term) in Wikipedia "Triangle graph", https://en.wikipedia.org/wiki/Triangle_graph, 27-Jul-2025: "In the mathematical field of graph theory, the triangle graph is a planar undirected graph with 3 vertices and 3 edges, in the form of a triangle. The triangle graph is also known as the cycle graph C3 and the complete graph K3." Often, however, the term "triangle" is also used to denote a corresponding subgraph of a given graph ("triangle in a graph"), see, for example, Wikipedia "Triangle-free graph", 28-Jul-2025, https://en.wikipedia.org/wiki/Triangle-free_graph: "In the mathematical area of graph theory, a triangle-free graph is an undirected graph in which no three vertices form a triangle of edges." In this subsection, a triangle (in a graph) is defined as a set of three vertices of a given graph. In this meaning, a triangle 𝑇 with (𝑇 ∈ (GrTriangles‘𝐺)) is neither a graph nor a subgraph, but it induces a triangle graph (𝐺 ISubGr 𝑇) as subgraph of the given graph 𝐺. We require that there are three (different) edges connecting the three (different) vertices of the triangle. Therefore, it is not sufficient for arbitrary hypergraphs to say "a triangle is a set of three (different) vertices connected with each other (by edges)", because there might be only one or two multiedges fulfilling this statement. We do not regard such degenerate cases as "triangle". The definition df-grtri 47905 is designed for a special purpose, namely to provide a criterion for two graphs being not isomorphic (see grimgrtri 47916). For other purposes, a more general definition might be useful, e.g., ComplSubGr = (𝑔 ∈ V, 𝑛 ∈ ℕ ↦ {𝑡 ∈ 𝒫 𝑣 ∣ ((♯‘𝑡) = 𝑛 ∧ (𝑔 ISubGr 𝑡) ∈ ComplGraph)}) for complete subgraphs of a given size (proposed by TA). With such a definition, we would have (GrTriangles‘𝐺) = (𝐺 ComplSubGr 3) (at least for simple graphs), and the definition df-grtri 47905 may become obsolete. | ||
| Syntax | cgrtri 47904 | Extend class notation with triangles (in a graph). |
| class GrTriangles | ||
| Definition | df-grtri 47905* | Definition of a triangles in a graph. A triangle in a graph is a set of three (different) vertices completely connected with each other. Such vertices induce a closed walk of length 3, see grtriclwlk3 47912, and the vertices of a cycle of size 3 are a triangle in a graph, see cycl3grtri 47914. (Contributed by AV, 20-Jul-2025.) |
| ⊢ GrTriangles = (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(Edg‘𝑔) / 𝑒⦌{𝑡 ∈ 𝒫 𝑣 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))}) | ||
| Theorem | grtriproplem 47906 | Lemma for grtriprop 47908. (Contributed by AV, 23-Jul-2025.) |
| ⊢ ((𝑓:(0..^3)–1-1-onto→{𝑥, 𝑦, 𝑧} ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝐸 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝐸 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝐸)) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) | ||
| Theorem | grtri 47907* | The triangles in a graph. (Contributed by AV, 20-Jul-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (GrTriangles‘𝐺) = {𝑡 ∈ 𝒫 𝑉 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝐸 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝐸 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝐸))}) | ||
| Theorem | grtriprop 47908* | The properties of a triangle. (Contributed by AV, 25-Jul-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑇 ∈ (GrTriangles‘𝐺) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑇 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑇) = 3 ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))) | ||
| Theorem | grtrif1o 47909 | Any bijection onto a triangle preserves the edges of the triangle. (Contributed by AV, 25-Jul-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝑇 ∈ (GrTriangles‘𝐺) ∧ 𝐹:(0..^3)–1-1-onto→𝑇) → ({(𝐹‘0), (𝐹‘1)} ∈ 𝐸 ∧ {(𝐹‘0), (𝐹‘2)} ∈ 𝐸 ∧ {(𝐹‘1), (𝐹‘2)} ∈ 𝐸)) | ||
| Theorem | isgrtri 47910* | A triangle in a graph. (Contributed by AV, 20-Jul-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑇 ∈ (GrTriangles‘𝐺) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑇 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑇) = 3 ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))) | ||
| Theorem | grtrissvtx 47911 | A triangle is a subset of the vertices (of a graph). (Contributed by AV, 26-Jul-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑇 ∈ (GrTriangles‘𝐺) → 𝑇 ⊆ 𝑉) | ||
| Theorem | grtriclwlk3 47912 | A triangle induces a closed walk of length 3 . (Contributed by AV, 26-Jul-2025.) |
| ⊢ (𝜑 → 𝑇 ∈ (GrTriangles‘𝐺)) & ⊢ (𝜑 → 𝑃:(0..^3)–1-1-onto→𝑇) ⇒ ⊢ (𝜑 → 𝑃 ∈ (3 ClWWalksN 𝐺)) | ||
| Theorem | cycl3grtrilem 47913 | Lemma for cycl3grtri 47914. (Contributed by AV, 5-Oct-2025.) |
| ⊢ (((𝐺 ∈ UPGraph ∧ 𝐹(Paths‘𝐺)𝑃) ∧ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ∧ (♯‘𝐹) = 3)) → ({(𝑃‘0), (𝑃‘1)} ∈ (Edg‘𝐺) ∧ {(𝑃‘0), (𝑃‘2)} ∈ (Edg‘𝐺) ∧ {(𝑃‘1), (𝑃‘2)} ∈ (Edg‘𝐺))) | ||
| Theorem | cycl3grtri 47914 | The vertices of a cycle of size 3 are a triangle in a graph. (Contributed by AV, 5-Oct-2025.) |
| ⊢ (𝜑 → 𝐺 ∈ UPGraph) & ⊢ (𝜑 → 𝐹(Cycles‘𝐺)𝑃) & ⊢ (𝜑 → (♯‘𝐹) = 3) ⇒ ⊢ (𝜑 → ran 𝑃 ∈ (GrTriangles‘𝐺)) | ||
| Theorem | grtrimap 47915 | Conditions for mapping triangles onto triangles. Lemma for grimgrtri 47916 and grlimgrtri 47963. (Contributed by AV, 23-Aug-2025.) |
| ⊢ (𝐹:𝑉–1-1→𝑊 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3)) → (((𝐹‘𝑎) ∈ 𝑊 ∧ (𝐹‘𝑏) ∈ 𝑊 ∧ (𝐹‘𝑐) ∈ 𝑊) ∧ (𝐹 “ 𝑇) = {(𝐹‘𝑎), (𝐹‘𝑏), (𝐹‘𝑐)} ∧ (♯‘(𝐹 “ 𝑇)) = 3))) | ||
| Theorem | grimgrtri 47916 | Graph isomorphisms map triangles onto triangles. (Contributed by AV, 27-Jul-2025.) (Proof shortened by AV, 24-Aug-2025.) |
| ⊢ (𝜑 → 𝐺 ∈ UHGraph) & ⊢ (𝜑 → 𝐻 ∈ UHGraph) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 GraphIso 𝐻)) & ⊢ (𝜑 → 𝑇 ∈ (GrTriangles‘𝐺)) ⇒ ⊢ (𝜑 → (𝐹 “ 𝑇) ∈ (GrTriangles‘𝐻)) | ||
| Theorem | usgrgrtrirex 47917* | Conditions for a simple graph to contain a triangle. (Contributed by AV, 7-Aug-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑁 = (𝐺 NeighbVtx 𝑎) ⇒ ⊢ (𝐺 ∈ USGraph → (∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))) | ||
According to Wikipedia "Star (graph theory)", 10-Sep-2025, https://en.wikipedia.org/wiki/Star_(graph_theory): "In graph theory, the star Sk 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 Sk to be the tree of order k with maximum diameter 2, in which case a star of k > 2 has k - 1 leaves.". | ||
| Syntax | cstgr 47918 | Extend class notation with star graphs. |
| class StarGr | ||
| Definition | df-stgr 47919* | Definition of star graphs according to the first definition in Wikipedia, so that (StarGr‘𝑁) has size 𝑁, and order 𝑁 + 1: (StarGr‘0) will be a single vertex (graph without edges), see stgr0 47927, (StarGr‘1) will be a single edge (graph with two vertices connected by an edge), see stgr1 47928, and (StarGr‘3) will be a 3-star or "claw" (a star with 3 edges). (Contributed by AV, 10-Sep-2025.) |
| ⊢ StarGr = (𝑛 ∈ ℕ0 ↦ {〈(Base‘ndx), (0...𝑛)〉, 〈(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})〉}) | ||
| Theorem | stgrfv 47920* | The star graph SN. (Contributed by AV, 10-Sep-2025.) |
| ⊢ (𝑁 ∈ ℕ0 → (StarGr‘𝑁) = {〈(Base‘ndx), (0...𝑁)〉, 〈(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})〉}) | ||
| Theorem | stgrvtx 47921 | The vertices of the star graph SN. (Contributed by AV, 11-Sep-2025.) |
| ⊢ (𝑁 ∈ ℕ0 → (Vtx‘(StarGr‘𝑁)) = (0...𝑁)) | ||
| Theorem | stgriedg 47922* | The indexed edges of the star graph SN. (Contributed by AV, 11-Sep-2025.) |
| ⊢ (𝑁 ∈ ℕ0 → (iEdg‘(StarGr‘𝑁)) = ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})) | ||
| Theorem | stgredg 47923* | The edges of the star graph SN. (Contributed by AV, 11-Sep-2025.) |
| ⊢ (𝑁 ∈ ℕ0 → (Edg‘(StarGr‘𝑁)) = {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}) | ||
| Theorem | stgredgel 47924* | An edge of the star graph SN. (Contributed by AV, 11-Sep-2025.) |
| ⊢ (𝑁 ∈ ℕ0 → (𝐸 ∈ (Edg‘(StarGr‘𝑁)) ↔ (𝐸 ⊆ (0...𝑁) ∧ ∃𝑥 ∈ (1...𝑁)𝐸 = {0, 𝑥}))) | ||
| Theorem | stgredgiun 47925* | The edges of the star graph SN as indexed union. (Contributed by AV, 29-Sep-2025.) |
| ⊢ (𝑁 ∈ ℕ0 → (Edg‘(StarGr‘𝑁)) = ∪ 𝑥 ∈ (1...𝑁){{0, 𝑥}}) | ||
| Theorem | stgrusgra 47926 | The star graph SN is a simple graph. (Contributed by AV, 11-Sep-2025.) |
| ⊢ (𝑁 ∈ ℕ0 → (StarGr‘𝑁) ∈ USGraph) | ||
| Theorem | stgr0 47927 | The star graph S0 consists of a single vertex without edges. (Contributed by AV, 11-Sep-2025.) |
| ⊢ (StarGr‘0) = {〈(Base‘ndx), {0}〉, 〈(.ef‘ndx), ∅〉} | ||
| Theorem | stgr1 47928 | The star graph S1 consists of a single simple edge. (Contributed by AV, 11-Sep-2025.) |
| ⊢ (StarGr‘1) = {〈(Base‘ndx), {0, 1}〉, 〈(.ef‘ndx), ( I ↾ {{0, 1}})〉} | ||
| Theorem | stgrvtx0 47929 | The center ("internal node") of a star graph SN. (Contributed by AV, 12-Sep-2025.) |
| ⊢ 𝐺 = (StarGr‘𝑁) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ ℕ0 → 0 ∈ 𝑉) | ||
| Theorem | stgrorder 47930 | The order of a star graph SN. (Contributed by AV, 12-Sep-2025.) |
| ⊢ 𝐺 = (StarGr‘𝑁) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ ℕ0 → (♯‘𝑉) = (𝑁 + 1)) | ||
| Theorem | stgrnbgr0 47931 | All vertices of a star graph SN except the center are in the (open) neighborhood of the center. (Contributed by AV, 12-Sep-2025.) |
| ⊢ 𝐺 = (StarGr‘𝑁) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝐺 NeighbVtx 0) = (𝑉 ∖ {0})) | ||
| Theorem | stgrclnbgr0 47932 | All vertices of a star graph SN are in the closed neighborhood of the center. (Contributed by AV, 12-Sep-2025.) |
| ⊢ 𝐺 = (StarGr‘𝑁) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝐺 ClNeighbVtx 0) = 𝑉) | ||
| Theorem | isubgr3stgrlem1 47933 | Lemma 1 for isubgr3stgr 47942. (Contributed by AV, 16-Sep-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝐹 = (𝐻 ∪ {〈𝑋, 𝑌〉}) ⇒ ⊢ ((𝐻:𝑈–1-1-onto→𝑅 ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅)) → 𝐹:𝐶–1-1-onto→(𝑅 ∪ {𝑌})) | ||
| Theorem | isubgr3stgrlem2 47934* | Lemma 2 for isubgr3stgr 47942. (Contributed by AV, 16-Sep-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑆 = (StarGr‘𝑁) & ⊢ 𝑊 = (Vtx‘𝑆) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ∃𝑓 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0})) | ||
| Theorem | isubgr3stgrlem3 47935* | Lemma 3 for isubgr3stgr 47942. (Contributed by AV, 17-Sep-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑆 = (StarGr‘𝑁) & ⊢ 𝑊 = (Vtx‘𝑆) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ∃𝑔(𝑔:𝐶–1-1-onto→𝑊 ∧ (𝑔‘𝑋) = 0)) | ||
| Theorem | isubgr3stgrlem4 47936* | Lemma 4 for isubgr3stgr 47942. (Contributed by AV, 24-Sep-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑆 = (StarGr‘𝑁) & ⊢ 𝑊 = (Vtx‘𝑆) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐴 = 𝑋 ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ∃𝑧 ∈ (1...𝑁)(𝐹 “ {𝐴, 𝐵}) = {0, 𝑧}) | ||
| Theorem | isubgr3stgrlem5 47937* | Lemma 5 for isubgr3stgr 47942. (Contributed by AV, 24-Sep-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑆 = (StarGr‘𝑁) & ⊢ 𝑊 = (Vtx‘𝑆) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶)) & ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖)) ⇒ ⊢ ((𝐹:𝐶⟶𝑊 ∧ 𝑌 ∈ 𝐼) → (𝐻‘𝑌) = (𝐹 “ 𝑌)) | ||
| Theorem | isubgr3stgrlem6 47938* | Lemma 6 for isubgr3stgr 47942. (Contributed by AV, 24-Sep-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑆 = (StarGr‘𝑁) & ⊢ 𝑊 = (Vtx‘𝑆) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶)) & ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖)) ⇒ ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 𝐻:𝐼⟶(Edg‘(StarGr‘𝑁))) | ||
| Theorem | isubgr3stgrlem7 47939* | Lemma 7 for isubgr3stgr 47942. (Contributed by AV, 29-Sep-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑆 = (StarGr‘𝑁) & ⊢ 𝑊 = (Vtx‘𝑆) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶)) & ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖)) ⇒ ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ 𝐽 ∈ (Edg‘(StarGr‘𝑁))) → (◡𝐹 “ 𝐽) ∈ 𝐼) | ||
| Theorem | isubgr3stgrlem8 47940* | Lemma 8 for isubgr3stgr 47942. (Contributed by AV, 29-Sep-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑆 = (StarGr‘𝑁) & ⊢ 𝑊 = (Vtx‘𝑆) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶)) & ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖)) ⇒ ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 𝐻:𝐼–1-1-onto→(Edg‘(StarGr‘𝑁))) | ||
| Theorem | isubgr3stgrlem9 47941* | Lemma 9 for isubgr3stgr 47942. (Contributed by AV, 29-Sep-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑆 = (StarGr‘𝑁) & ⊢ 𝑊 = (Vtx‘𝑆) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶)) & ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖)) ⇒ ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐻:𝐼–1-1-onto→(Edg‘(StarGr‘𝑁)) ∧ ∀𝑒 ∈ 𝐼 (𝐹 “ 𝑒) = (𝐻‘𝑒))) | ||
| Theorem | isubgr3stgr 47942* | If a vertex of a simple graph has exactly 𝑁 (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 𝑁-star. (Contributed by AV, 29-Sep-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑆 = (StarGr‘𝑁) & ⊢ 𝑊 = (Vtx‘𝑆) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸) → (𝐺 ISubGr 𝐶) ≃𝑔𝑟 (StarGr‘𝑁))) | ||
This section is about local isomorphisms of graphs, which are a generalization of isomorphisms of graphs, i.e., every isomorphism between two graphs is also a local isomorphism between these graphs, see uhgrimgrlim 47954. This definition is according to a chat in mathoverflow (https://mathoverflow.net/questions/491133/locally-isomorphic-graphs 47954): roughly speaking, it restricts the correspondence of two graphs to their neighborhoods. Additionally, a binary relation ≃𝑙𝑔𝑟 is defined (see df-grlic 47948) which is true for two graphs iff there is a local isomorphism between these graphs. Then these graphs are called "locally isomorphic". Therefore, this relation is also called "is locally isomorphic to" relation. As a main result of this section, it is shown that the "is locally isomorphic to" relation is an equivalence relation (for hypergraphs), see grlicer 47976. The names and symbols are chosen analogously to group isomorphisms GrpIso (see df-gim 19277) and graph isomorphisms GraphIso (see df-grim 47864) resp. isomorphism between groups ≃𝑔 (see df-gic 19278) and isomorphism between graphs ≃𝑔𝑟 (see df-gric 47867). In the future, it should be shown that there are local isomorphisms between two graphs which are not (ordinary) isomorphisms between these graphs, as discussed in the above mentioned chat in mathoverflow. | ||
| Syntax | cgrlim 47943 | The class of graph local isomorphism sets. |
| class GraphLocIso | ||
| Syntax | cgrlic 47944 | The class of the graph local isomorphism relation. |
| class ≃𝑙𝑔𝑟 | ||
| Definition | df-grlim 47945* | A local isomorphism of graphs is a bijection between the sets of vertices of two graphs that preserves local adjacency, i.e. the subgraph induced by the closed neighborhood of a vertex of the first graph and the subgraph induced by the closed neighborhood of the associated vertex of the second graph are isomorphic. See the following chat in mathoverflow: https://mathoverflow.net/questions/491133/locally-isomorphic-graphs. (Contributed by AV, 27-Apr-2025.) |
| ⊢ GraphLocIso = (𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ∧ ∀𝑣 ∈ (Vtx‘𝑔)(𝑔 ISubGr (𝑔 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (ℎ ISubGr (ℎ ClNeighbVtx (𝑓‘𝑣))))}) | ||
| Theorem | grlimfn 47946 | The graph local isomorphism function is a well-defined function. (Contributed by AV, 20-May-2025.) |
| ⊢ GraphLocIso Fn (V × V) | ||
| Theorem | grlimdmrel 47947 | The domain of the graph local isomorphism function is a relation. (Contributed by AV, 20-May-2025.) |
| ⊢ Rel dom GraphLocIso | ||
| Definition | df-grlic 47948 | Two graphs are said to be locally isomorphic iff they are connected by at least one local isomorphism. (Contributed by AV, 27-Apr-2025.) |
| ⊢ ≃𝑙𝑔𝑟 = (◡ GraphLocIso “ (V ∖ 1o)) | ||
| Theorem | isgrlim 47949* | A local isomorphism of graphs is a bijection between their vertices that preserves neighborhoods. (Contributed by AV, 20-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) ⇒ ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍) → (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣)))))) | ||
| Theorem | isgrlim2 47950* | A local isomorphism of graphs is a bijection between their vertices that preserves neighborhoods. Definitions expanded. (Contributed by AV, 29-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑣) & ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑣)) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐽 = (iEdg‘𝐻) & ⊢ 𝐾 = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) ⊆ 𝑁} & ⊢ 𝐿 = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) ⊆ 𝑀} ⇒ ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍) → (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖))))))) | ||
| Theorem | grlimprop 47951* | Properties of a local isomorphism of graphs. (Contributed by AV, 21-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) ⇒ ⊢ (𝐹 ∈ (𝐺 GraphLocIso 𝐻) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (𝐻 ISubGr (𝐻 ClNeighbVtx (𝐹‘𝑣))))) | ||
| Theorem | grlimf1o 47952 | A local isomorphism of graphs is a bijection between their vertices. (Contributed by AV, 21-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) ⇒ ⊢ (𝐹 ∈ (𝐺 GraphLocIso 𝐻) → 𝐹:𝑉–1-1-onto→𝑊) | ||
| Theorem | grlimprop2 47953* | Properties of a local isomorphism of graphs. (Contributed by AV, 29-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑣) & ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑣)) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐽 = (iEdg‘𝐻) & ⊢ 𝐾 = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) ⊆ 𝑁} & ⊢ 𝐿 = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) ⊆ 𝑀} ⇒ ⊢ (𝐹 ∈ (𝐺 GraphLocIso 𝐻) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))))) | ||
| Theorem | uhgrimgrlim 47954 | An isomorphism of hypergraphs is a local isomorphism between the two graphs. (Contributed by AV, 2-Jun-2025.) |
| ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → 𝐹 ∈ (𝐺 GraphLocIso 𝐻)) | ||
| Theorem | uspgrlimlem1 47955* | Lemma 1 for uspgrlim 47959. (Contributed by AV, 16-Aug-2025.) |
| ⊢ 𝑀 = (𝐻 ClNeighbVtx 𝑋) & ⊢ 𝐽 = (Edg‘𝐻) & ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀} ⇒ ⊢ (𝐻 ∈ USPGraph → 𝐿 = ((iEdg‘𝐻) “ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀})) | ||
| Theorem | uspgrlimlem2 47956* | Lemma 2 for uspgrlim 47959. (Contributed by AV, 16-Aug-2025.) |
| ⊢ 𝑀 = (𝐻 ClNeighbVtx 𝑋) & ⊢ 𝐽 = (Edg‘𝐻) & ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀} ⇒ ⊢ (𝐻 ∈ USPGraph → (◡(iEdg‘𝐻) “ 𝐿) = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}) | ||
| Theorem | uspgrlimlem3 47957* | Lemma 3 for uspgrlim 47959. (Contributed by AV, 16-Aug-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑣) & ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑣)) & ⊢ 𝐼 = (Edg‘𝐺) & ⊢ 𝐽 = (Edg‘𝐻) & ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁} & ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀} ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ ℎ:{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁}–1-1-onto→𝑅 ∧ ∀𝑖 ∈ {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) ⊆ 𝑁} (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(ℎ‘𝑖))) → (𝑒 ∈ 𝐾 → (𝑓 “ 𝑒) = ((((iEdg‘𝐻) ∘ ℎ) ∘ ◡(iEdg‘𝐺))‘𝑒))) | ||
| Theorem | uspgrlimlem4 47958* | Lemma 4 for uspgrlim 47959. (Contributed by AV, 16-Aug-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑣) & ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑣)) & ⊢ 𝐼 = (Edg‘𝐺) & ⊢ 𝐽 = (Edg‘𝐻) & ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁} & ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀} ⇒ ⊢ (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ (𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((𝑖 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑖) ⊆ 𝑁) → (𝑓 “ ((iEdg‘𝐺)‘𝑖)) = ((iEdg‘𝐻)‘(((◡(iEdg‘𝐻) ∘ 𝑔) ∘ (iEdg‘𝐺))‘𝑖)))) | ||
| Theorem | uspgrlim 47959* | A local isomorphism of simple pseudographs is a bijection between their vertices that preserves neighborhoods, expressed by properties of their edges (not edge functions as in isgrlim2 47950). (Contributed by AV, 15-Aug-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑣) & ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑣)) & ⊢ 𝐼 = (Edg‘𝐺) & ⊢ 𝐽 = (Edg‘𝐻) & ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁} & ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀} ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑍) → (𝐹 ∈ (𝐺 GraphLocIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))) | ||
| Theorem | usgrlimprop 47960* | Properties of a local isomorphism of simple pseudographs. (Contributed by AV, 17-Aug-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑣) & ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑣)) & ⊢ 𝐼 = (Edg‘𝐺) & ⊢ 𝐽 = (Edg‘𝐻) & ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁} & ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀} ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ (𝐺 GraphLocIso 𝐻)) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑒 ∈ 𝐾 (𝑓 “ 𝑒) = (𝑔‘𝑒))))) | ||
| Theorem | grlimgrtrilem1 47961* | Lemma 3 for grlimgrtri 47963. (Contributed by AV, 24-Aug-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑎) & ⊢ 𝐼 = (Edg‘𝐺) & ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁} ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ ({𝑎, 𝑏} ∈ 𝐼 ∧ {𝑎, 𝑐} ∈ 𝐼 ∧ {𝑏, 𝑐} ∈ 𝐼)) → ({𝑎, 𝑏} ∈ 𝐾 ∧ {𝑎, 𝑐} ∈ 𝐾 ∧ {𝑏, 𝑐} ∈ 𝐾)) | ||
| Theorem | grlimgrtrilem2 47962* | Lemma 3 for grlimgrtri 47963. (Contributed by AV, 23-Aug-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑎) & ⊢ 𝐼 = (Edg‘𝐺) & ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁} & ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑎)) & ⊢ 𝐽 = (Edg‘𝐻) & ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀} ⇒ ⊢ (((𝑓:𝑁–1-1-onto→𝑀 ∧ 𝑔:𝐾–1-1-onto→𝐿) ∧ ∀𝑖 ∈ 𝐾 (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑏, 𝑐} ∈ 𝐾) → {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ 𝐽) | ||
| Theorem | grlimgrtri 47963* | Local isomorphisms between simple pseudographs map triangles onto triangles. (Contributed by AV, 24-Aug-2025.) |
| ⊢ (𝜑 → 𝐺 ∈ USPGraph) & ⊢ (𝜑 → 𝐻 ∈ USPGraph) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 GraphLocIso 𝐻)) & ⊢ (𝜑 → 𝑇 ∈ (GrTriangles‘𝐺)) ⇒ ⊢ (𝜑 → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐻)) | ||
| Theorem | brgrlic 47964 | The relation "is locally isomorphic to" for graphs. (Contributed by AV, 9-Jun-2025.) |
| ⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 ↔ (𝑅 GraphLocIso 𝑆) ≠ ∅) | ||
| Theorem | brgrilci 47965 | Prove that two graphs are locally isomorphic by an explicit local isomorphism. (Contributed by AV, 9-Jun-2025.) |
| ⊢ (𝐹 ∈ (𝑅 GraphLocIso 𝑆) → 𝑅 ≃𝑙𝑔𝑟 𝑆) | ||
| Theorem | grlicrel 47966 | The "is locally isomorphic to" relation for graphs is a relation. (Contributed by AV, 9-Jun-2025.) |
| ⊢ Rel ≃𝑙𝑔𝑟 | ||
| Theorem | grlicrcl 47967 | Reverse closure of the "is locally isomorphic to" relation for graphs. (Contributed by AV, 9-Jun-2025.) |
| ⊢ (𝐺 ≃𝑙𝑔𝑟 𝑆 → (𝐺 ∈ V ∧ 𝑆 ∈ V)) | ||
| Theorem | dfgrlic2 47968* | Alternate, explicit definition of the "is locally isomorphic to" relation for two graphs. (Contributed by AV, 9-Jun-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) ⇒ ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌) → (𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣)))))) | ||
| Theorem | grilcbri 47969* | Implications of two graphs being locally isomorphic. (Contributed by AV, 9-Jun-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) ⇒ ⊢ (𝐺 ≃𝑙𝑔𝑟 𝐻 → ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑣))))) | ||
| Theorem | dfgrlic3 47970* | Alternate, explicit definition of the "is locally isomorphic to" relation for two graphs. (Contributed by AV, 9-Jun-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐽 = (iEdg‘𝐻) & ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑣) & ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝑓‘𝑣)) & ⊢ 𝐾 = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) ⊆ 𝑁} & ⊢ 𝐿 = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) ⊆ 𝑀} ⇒ ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌) → (𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑣 ∈ 𝑉 ∃𝑗(𝑗:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑗 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖))))))) | ||
| Theorem | grilcbri2 47971* | Implications of two graphs being locally isomorphic. (Contributed by AV, 9-Jun-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐽 = (iEdg‘𝐻) & ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝑓‘𝑋)) & ⊢ 𝐾 = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) ⊆ 𝑁} & ⊢ 𝐿 = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) ⊆ 𝑀} ⇒ ⊢ (𝐺 ≃𝑙𝑔𝑟 𝐻 → ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ (𝑋 ∈ 𝑉 → ∃𝑗(𝑗:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑗 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖))))))) | ||
| Theorem | grlicref 47972 | Graph local isomorphism is reflexive for hypergraphs. (Contributed by AV, 9-Jun-2025.) |
| ⊢ (𝐺 ∈ UHGraph → 𝐺 ≃𝑙𝑔𝑟 𝐺) | ||
| Theorem | grlicsym 47973 | Graph local isomorphism is symmetric for hypergraphs. (Contributed by AV, 9-Jun-2025.) |
| ⊢ (𝐺 ∈ UHGraph → (𝐺 ≃𝑙𝑔𝑟 𝑆 → 𝑆 ≃𝑙𝑔𝑟 𝐺)) | ||
| Theorem | grlicsymb 47974 | Graph local isomorphism is symmetric in both directions for hypergraphs. (Contributed by AV, 9-Jun-2025.) |
| ⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph) → (𝐴 ≃𝑙𝑔𝑟 𝐵 ↔ 𝐵 ≃𝑙𝑔𝑟 𝐴)) | ||
| Theorem | grlictr 47975 | Graph local isomorphism is transitive. (Contributed by AV, 10-Jun-2025.) |
| ⊢ ((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) → 𝑅 ≃𝑙𝑔𝑟 𝑇) | ||
| Theorem | grlicer 47976 | Local isomorphism is an equivalence relation on hypergraphs. (Contributed by AV, 11-Jun-2025.) |
| ⊢ ( ≃𝑙𝑔𝑟 ∩ (UHGraph × UHGraph)) Er UHGraph | ||
| Theorem | grlicen 47977 | Locally isomorphic graphs have equinumerous sets of vertices. (Contributed by AV, 11-Jun-2025.) |
| ⊢ 𝐵 = (Vtx‘𝑅) & ⊢ 𝐶 = (Vtx‘𝑆) ⇒ ⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 → 𝐵 ≈ 𝐶) | ||
| Theorem | gricgrlic 47978 | Isomorphic hypergraphs are locally isomorphic. (Contributed by AV, 12-Jun-2025.) (Proof shortened by AV, 11-Jul-2025.) |
| ⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) → (𝐺 ≃𝑔𝑟 𝐻 → 𝐺 ≃𝑙𝑔𝑟 𝐻)) | ||
| Theorem | clnbgr3stgrgrlic 47979* | If all (closed) neighborhoods of the vertices in two simple graphs with the same order induce a subgraph which is isomorphic to an 𝑁-star, then the two graphs are locally isomorphic. (Contributed by AV, 29-Sep-2025.) |
| ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) ⇒ ⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉 ≈ 𝑊) ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟 (StarGr‘𝑁) ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟 (StarGr‘𝑁)) → 𝐺 ≃𝑙𝑔𝑟 𝐻) | ||
| Theorem | usgrexmpl1lem 47980* | Lemma for usgrexmpl1 47981. (Contributed by AV, 2-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉 ⇒ ⊢ 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} | ||
| Theorem | usgrexmpl1 47981 | 𝐺 is a simple graph of six vertices 0, 1, 2, 3, 4, 5, with edges {0, 1}, {1, 2}, {0, 2}, {0, 3}, {3, 4}, {3, 5}, {4, 5}. (Contributed by AV, 3-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ 𝐺 ∈ USGraph | ||
| Theorem | usgrexmpl1vtx 47982 | The vertices 0, 1, 2, 3, 4, 5 of the graph 𝐺 = 〈𝑉, 𝐸〉. (Contributed by AV, 3-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ (Vtx‘𝐺) = ({0, 1, 2} ∪ {3, 4, 5}) | ||
| Theorem | usgrexmpl1edg 47983 | The edges {0, 1}, {1, 2}, {0, 2}, {0, 3}, {3, 4}, {3, 5}, {4, 5} of the graph 𝐺 = 〈𝑉, 𝐸〉. (Contributed by AV, 3-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ (Edg‘𝐺) = ({{0, 3}} ∪ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{3, 4}, {3, 5}, {4, 5}})) | ||
| Theorem | usgrexmpl1tri 47984 | 𝐺 contains a triangle 0, 1, 2, with corresponding edges {0, 1}, {1, 2}, {0, 2}. (Contributed by AV, 3-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ {0, 1, 2} ∈ (GrTriangles‘𝐺) | ||
| Theorem | usgrexmpl2lem 47985* | Lemma for usgrexmpl2 47986. (Contributed by AV, 3-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 ⇒ ⊢ 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} | ||
| Theorem | usgrexmpl2 47986 | 𝐺 is a simple graph of six vertices 0, 1, 2, 3, 4, 5, with edges {0, 1}, {1, 2}, {2, 3}, {0, 3}, {3, 4}, {4, 5}, {0, 5}. (Contributed by AV, 3-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ 𝐺 ∈ USGraph | ||
| Theorem | usgrexmpl2vtx 47987 | The vertices 0, 1, 2, 3, 4, 5 of the graph 𝐺 = 〈𝑉, 𝐸〉. (Contributed by AV, 3-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ (Vtx‘𝐺) = ({0, 1, 2} ∪ {3, 4, 5}) | ||
| Theorem | usgrexmpl2edg 47988 | The edges {0, 1}, {1, 2}, {2, 3}, {0, 3}, {3, 4}, {4, 5}, {0, 5} of the graph 𝐺 = 〈𝑉, 𝐸〉. (Contributed by AV, 3-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ (Edg‘𝐺) = ({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}})) | ||
| Theorem | usgrexmpl2nblem 47989* | Lemma for usgrexmpl2nb0 47990 etc. (Contributed by AV, 9-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ (𝐾 ∈ ({0, 1, 2} ∪ {3, 4, 5}) → (𝐺 NeighbVtx 𝐾) = {𝑛 ∈ ({0, 1, 2} ∪ {3, 4, 5}) ∣ {𝐾, 𝑛} ∈ ({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))}) | ||
| Theorem | usgrexmpl2nb0 47990 | The neighborhood of the first vertex of graph 𝐺. (Contributed by AV, 9-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ (𝐺 NeighbVtx 0) = {1, 3, 5} | ||
| Theorem | usgrexmpl2nb1 47991 | The neighborhood of the second vertex of graph 𝐺. (Contributed by AV, 9-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ (𝐺 NeighbVtx 1) = {0, 2} | ||
| Theorem | usgrexmpl2nb2 47992 | The neighborhood of the third vertex of graph 𝐺. (Contributed by AV, 9-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ (𝐺 NeighbVtx 2) = {1, 3} | ||
| Theorem | usgrexmpl2nb3 47993 | The neighborhood of the forth vertex of graph 𝐺. (Contributed by AV, 9-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ (𝐺 NeighbVtx 3) = {0, 2, 4} | ||
| Theorem | usgrexmpl2nb4 47994 | The neighborhood of the fifth vertex of graph 𝐺. (Contributed by AV, 9-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ (𝐺 NeighbVtx 4) = {3, 5} | ||
| Theorem | usgrexmpl2nb5 47995 | The neighborhood of the sixth vertex of graph 𝐺. (Contributed by AV, 10-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ (𝐺 NeighbVtx 5) = {0, 4} | ||
| Theorem | usgrexmpl2trifr 47996* | 𝐺 is triangle-free. (Contributed by AV, 10-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ ¬ ∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) | ||
| Theorem | usgrexmpl12ngric 47997 | The graphs 𝐻 and 𝐺 are not isomorphic (𝐻 contains a triangle, see usgrexmpl1tri 47984, whereas 𝐺 does not, see usgrexmpl2trifr 47996. (Contributed by AV, 10-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 & ⊢ 𝐾 = 〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉 & ⊢ 𝐻 = 〈𝑉, 𝐾〉 ⇒ ⊢ ¬ 𝐺 ≃𝑔𝑟 𝐻 | ||
| Theorem | usgrexmpl12ngrlic 47998 | The graphs 𝐻 and 𝐺 are not locally isomorphic (𝐻 contains a triangle, see usgrexmpl1tri 47984, whereas 𝐺 does not, see usgrexmpl2trifr 47996. (Contributed by AV, 24-Aug-2025.) |
| ⊢ 𝑉 = (0...5) & ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 & ⊢ 𝐾 = 〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉 & ⊢ 𝐻 = 〈𝑉, 𝐾〉 ⇒ ⊢ ¬ 𝐺 ≃𝑙𝑔𝑟 𝐻 | ||
According to Wikipedia "Generalized Petersen graph", 26-Aug-2025, https://en.wikipedia.org/wiki/Generalized_Petersen_graph: "In graph theory, the generalized Petersen graphs are a family of cubic graphs formed by connecting the vertices of a regular polygon to the corresponding vertices of a star polygon. They include the Petersen graph and generalize one of the ways of constructing the Petersen graph. ... Among the generalized Petersen graphs are the n-prism, ...". The vertices of the regular polygon are called "outside vertices", the vertices of the star polygon "inside vertices" (see A. Steimle, W. Stanton, "The isomorphism classes of the generalized Petersen graphs", Discrete Mathematics Volume 309, Issue 1, 6 January 2009, Pages 231-237: https://doi.org/10.1016/j.disc.2007.12.074). Since regular polygons are also considered as star polygons (with density 1), many theorems for "inside vertices" (with labels containing the fragment "vtx1") can be specialized for "outside vertices" (with labels containing the fragment "vtx0"). | ||
| Syntax | cgpg 47999 | Extend class notation with generalized Petersen graphs. |
| class gPetersenGr | ||
| Definition | df-gpg 48000* |
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, 𝐺(𝑛, 𝑘) is a graph with vertex set {
u0,
u1, ... , un-1, v0, v1, ... , vn-1 } and
edge set { ui ui+1 , ui
vi , vi vi+k | 0 ≤ 𝑖 ≤
(𝑛 − 1) }
where subscripts are to be
read modulo n and where 𝑘 < (𝑛 / 2). Some authors use the
notation GPG(n,k)."
Instead of 𝑛 ∈ ℕ, we could restrict the first argument to 𝑛 ∈ (ℤ≥‘3) (i.e., 3 ≤ 𝑛), because for 𝑛 ≤ 2, the definition is not meaningful (since then (⌈‘(𝑛 / 2)) ≤ 1 and therefore (1..^(⌈‘(𝑛 / 2))) = ∅, so that there would be no fitting second argument). (Contributed by AV, 26-Aug-2025.) |
| ⊢ gPetersenGr = (𝑛 ∈ ℕ, 𝑘 ∈ (1..^(⌈‘(𝑛 / 2))) ↦ {〈(Base‘ndx), ({0, 1} × (0..^𝑛))〉, 〈(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 ({0, 1} × (0..^𝑛)) ∣ ∃𝑥 ∈ (0..^𝑛)(𝑒 = {〈0, 𝑥〉, 〈0, ((𝑥 + 1) mod 𝑛)〉} ∨ 𝑒 = {〈0, 𝑥〉, 〈1, 𝑥〉} ∨ 𝑒 = {〈1, 𝑥〉, 〈1, ((𝑥 + 𝑘) mod 𝑛)〉})})〉}) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |