| Metamath
Proof Explorer Theorem List (p. 479 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 | ||
| Axiom | ax-hgprmladder 47801 | There is a partition ("ladder") of primes from 7 to 8.8 x 10^30 with parts ("rungs") having lengths of at least 4 and at most N - 4, see section 1.2.2 in [Helfgott] p. 4. Temporarily provided as "axiom". (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
| ⊢ ∃𝑑 ∈ (ℤ≥‘3)∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)))) | ||
| Theorem | tgblthelfgott 47802 | The ternary Goldbach conjecture is valid for all odd numbers less than 8.8 x 10^30 (actually 8.875694 x 10^30, see section 1.2.2 in [Helfgott] p. 4, using bgoldbachlt 47800, ax-hgprmladder 47801 and bgoldbtbnd 47796. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
| ⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29))) → 𝑁 ∈ GoldbachOdd ) | ||
| Theorem | tgoldbachlt 47803* | The ternary Goldbach conjecture is valid for small odd numbers (i.e. for all odd numbers less than a fixed big 𝑚 greater than 8 x 10^30). This is verified for m = 8.875694 x 10^30 by Helfgott, see tgblthelfgott 47802. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
| ⊢ ∃𝑚 ∈ ℕ ((8 · (;10↑;30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd )) | ||
| Theorem | tgoldbach 47804 | The ternary Goldbach conjecture is valid. Main theorem in [Helfgott] p. 2. This follows from tgoldbachlt 47803 and ax-tgoldbachgt 47798. (Contributed by AV, 2-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
| ⊢ ∀𝑛 ∈ Odd (7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) | ||
| Syntax | cclnbgr 47805 | Extend class notation with closed neighborhoods (of a vertex in a graph). |
| class ClNeighbVtx | ||
| Definition | df-clnbgr 47806* | Define the closed neighborhood resp. the class of all neighbors of a vertex (in a graph) and the vertex itself, see definition in section I.1 of [Bollobas] p. 3. The closed neighborhood of a vertex is the set of all vertices which are connected with this vertex by an edge and the vertex itself (in contrast to an open neighborhood, see df-nbgr 29350). Alternatively, a closed neighborhood of a vertex could have been defined as its open neighborhood enhanced by the vertex itself, see dfclnbgr4 47811. This definition is applicable even for arbitrary hypergraphs. (Contributed by AV, 7-May-2025.) |
| ⊢ ClNeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒})) | ||
| Theorem | clnbgrprc0 47807 | The closed neighborhood is empty if the graph 𝐺 or the vertex 𝑁 are proper classes. (Contributed by AV, 7-May-2025.) |
| ⊢ (¬ (𝐺 ∈ V ∧ 𝑁 ∈ V) → (𝐺 ClNeighbVtx 𝑁) = ∅) | ||
| Theorem | clnbgrcl 47808 | If a class 𝑋 has at least one element in its closed neighborhood, this class must be a vertex. (Contributed by AV, 7-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ (𝐺 ClNeighbVtx 𝑋) → 𝑋 ∈ 𝑉) | ||
| Theorem | clnbgrval 47809* | The closed neighborhood of a vertex 𝑉 in a graph 𝐺. (Contributed by AV, 7-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒})) | ||
| Theorem | dfclnbgr2 47810* | Alternate definition of the closed neighborhood of a vertex breaking up the subset relationship of an unordered pair. (Contributed by AV, 7-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)})) | ||
| Theorem | dfclnbgr4 47811 | Alternate definition of the closed neighborhood of a vertex as union of the vertex with its open neighborhood. (Contributed by AV, 8-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ (𝐺 NeighbVtx 𝑁))) | ||
| Theorem | elclnbgrelnbgr 47812 | 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.) |
| ⊢ ((𝑋 ∈ (𝐺 ClNeighbVtx 𝑁) ∧ 𝑋 ≠ 𝑁) → 𝑋 ∈ (𝐺 NeighbVtx 𝑁)) | ||
| Theorem | dfclnbgr3 47813* | Alternate definition of the closed neighborhood of a vertex using the edge function instead of the edges themselves (see also clnbgrval 47809). (Contributed by AV, 8-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝑁 ∈ 𝑉 ∧ Fun 𝐼) → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑖 ∈ dom 𝐼{𝑁, 𝑛} ⊆ (𝐼‘𝑖)})) | ||
| Theorem | clnbgrnvtx0 47814 | If a class 𝑋 is not a vertex of a graph 𝐺, then it has an empty closed neighborhood in 𝐺. (Contributed by AV, 8-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑋 ∉ 𝑉 → (𝐺 ClNeighbVtx 𝑋) = ∅) | ||
| Theorem | clnbgrel 47815* | Characterization of a member 𝑁 of the closed neighborhood of a vertex 𝑋 in a graph 𝐺. (Contributed by AV, 9-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑁 ∈ (𝐺 ClNeighbVtx 𝑋) ↔ ((𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ (𝑁 = 𝑋 ∨ ∃𝑒 ∈ 𝐸 {𝑋, 𝑁} ⊆ 𝑒))) | ||
| Theorem | clnbgrvtxel 47816 | Every vertex 𝐾 is a member of its closed neighborhood. (Contributed by AV, 10-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ (𝐺 ClNeighbVtx 𝐾)) | ||
| Theorem | clnbgrisvtx 47817 | Every member 𝑁 of the closed neighborhood of a vertex 𝐾 is a vertex. (Contributed by AV, 9-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ (𝐺 ClNeighbVtx 𝐾) → 𝑁 ∈ 𝑉) | ||
| Theorem | clnbgrssvtx 47818 | The closed neighborhood of a vertex 𝐾 in a graph is a subset of all vertices of the graph. (Contributed by AV, 9-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ClNeighbVtx 𝐾) ⊆ 𝑉 | ||
| Theorem | clnbgrn0 47819 | The closed neighborhood of a vertex is never empty. (Contributed by AV, 16-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) ≠ ∅) | ||
| Theorem | clnbupgr 47820* | The closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸})) | ||
| Theorem | clnbupgrel 47821 | A member of the closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → (𝑁 ∈ (𝐺 ClNeighbVtx 𝐾) ↔ (𝑁 = 𝐾 ∨ {𝑁, 𝐾} ∈ 𝐸))) | ||
| Theorem | clnbgr0vtx 47822 | In a null graph (with no vertices), all closed neighborhoods are empty. (Contributed by AV, 15-Nov-2020.) |
| ⊢ ((Vtx‘𝐺) = ∅ → (𝐺 ClNeighbVtx 𝐾) = ∅) | ||
| Theorem | clnbgr0edg 47823 | In an empty graph (with no edges), all closed neighborhoods consists of a single vertex. (Contributed by AV, 10-May-2025.) |
| ⊢ (((Edg‘𝐺) = ∅ ∧ 𝐾 ∈ (Vtx‘𝐺)) → (𝐺 ClNeighbVtx 𝐾) = {𝐾}) | ||
| Theorem | clnbgrsym 47824 | In a graph, the closed neighborhood relation is symmetric: a vertex 𝑁 in a graph 𝐺 is a neighbor of a second vertex 𝐾 iff the second vertex 𝐾 is a neighbor of the first vertex 𝑁. (Contributed by AV, 10-May-2025.) |
| ⊢ (𝑁 ∈ (𝐺 ClNeighbVtx 𝐾) ↔ 𝐾 ∈ (𝐺 ClNeighbVtx 𝑁)) | ||
| Theorem | predgclnbgrel 47825 | If a (not necessarily proper) unordered pair containing a vertex is an edge, the other vertex is in the closed neighborhood of the first vertex. (Contributed by AV, 23-Aug-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ {𝑋, 𝑁} ∈ 𝐸) → 𝑁 ∈ (𝐺 ClNeighbVtx 𝑋)) | ||
| Theorem | clnbgredg 47826 | A vertex connected by an edge with another vertex is a neighbor of that vertex. (Contributed by AV, 24-Aug-2025.) |
| ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑋) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ (𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾)) → 𝑌 ∈ 𝑁) | ||
| Theorem | clnbgrssedg 47827 | The vertices connected by an edge are a subset of the neighborhood of each of these vertices. (Contributed by AV, 26-May-2025.) (Proof shortened by AV, 24-Aug-2025.) |
| ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑋) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾) → 𝐾 ⊆ 𝑁) | ||
| Theorem | edgusgrclnbfin 47828* | The size of the closed neighborhood of a vertex in a simple graph is finite iff the number of edges having this vertex as endpoint is finite. (Contributed by AV, 10-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ((𝐺 ClNeighbVtx 𝑈) ∈ Fin ↔ {𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒} ∈ Fin)) | ||
| Theorem | clnbusgrfi 47829 | The closed neighborhood of a vertex in a simple graph with a finite number of edges is a finite set. (Contributed by AV, 10-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐸 ∈ Fin ∧ 𝑈 ∈ 𝑉) → (𝐺 ClNeighbVtx 𝑈) ∈ Fin) | ||
| Theorem | clnbfiusgrfi 47830 | The closed neighborhood of a vertex in a finite simple graph is a finite set. (Contributed by AV, 10-May-2025.) |
| ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ (Vtx‘𝐺)) → (𝐺 ClNeighbVtx 𝑁) ∈ Fin) | ||
| Theorem | clnbgrlevtx 47831 | The size of the closed neighborhood of a vertex is at most the number of vertices of a graph. (Contributed by AV, 10-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (♯‘(𝐺 ClNeighbVtx 𝑈)) ≤ (♯‘𝑉) | ||
We have already definitions for open and closed neighborhoods of a vertex, which differs only in the fact that the first never contains the vertex, and the latter always contains the vertex. One of these definitions, however, cannot be simply derived from the other. This would be possible if a definition of a semiclosed neighborhood was available, see dfsclnbgr2 47832. The definitions for open and closed neighborhoods could be derived from such a more simple, but otherwise probably useless definition, see dfnbgr5 47837 and dfclnbgr5 47836. Depending on the existence of certain edges, a vertex belongs to its semiclosed neighborhood or not. An alternate approach is to introduce semiopen neighborhoods, see dfvopnbgr2 47839. The definitions for open and closed neighborhoods could also be derived from such a definition, see dfnbgr6 47843 and dfclnbgr6 47842. Like with semiclosed neighborhood, depending on the existence of certain edges, a vertex belongs to its semiopen neighborhood or not. It is unclear if either definition is/will be useful, and in contrast to dfsclnbgr2 47832, the definition of semiopen neighborhoods is much more complex. | ||
| Theorem | dfsclnbgr2 47832* | Alternate definition of the semiclosed neighborhood of a vertex breaking up the subset relationship of an unordered pair. A semiclosed neighborhood 𝑆 of a vertex 𝑁 is the set of all vertices incident with edges which join the vertex 𝑁 with a vertex. Therefore, a vertex is contained in its semiclosed neighborhood if it is connected with any vertex by an edge (see sclnbgrelself 47834), even only with itself (i.e., by a loop). (Contributed by AV, 16-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒} & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)}) | ||
| Theorem | sclnbgrel 47833* | Characterization of a member 𝑋 of the semiclosed neighborhood of a vertex 𝑁 in a graph 𝐺. (Contributed by AV, 16-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒} & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝑆 ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑋} ⊆ 𝑒)) | ||
| Theorem | sclnbgrelself 47834* | A vertex 𝑁 is a member of its semiclosed neighborhood iff there is an edge joining the vertex with a vertex. (Contributed by AV, 16-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒} & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑆 ↔ (𝑁 ∈ 𝑉 ∧ ∃𝑒 ∈ 𝐸 𝑁 ∈ 𝑒)) | ||
| Theorem | sclnbgrisvtx 47835* | Every member 𝑋 of the semiclosed neighborhood of a vertex 𝑁 is a vertex. (Contributed by AV, 16-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒} & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝑆 → 𝑋 ∈ 𝑉) | ||
| Theorem | dfclnbgr5 47836* | Alternate definition of the closed neighborhood of a vertex as union of the vertex with its semiclosed neighborhood. (Contributed by AV, 16-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒} & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ 𝑆)) | ||
| Theorem | dfnbgr5 47837* | Alternate definition of the (open) neighborhood of a vertex as a semiclosed neighborhood without itself. (Contributed by AV, 16-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒} & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐺 NeighbVtx 𝑁) = (𝑆 ∖ {𝑁})) | ||
| Theorem | dfnbgrss 47838* | Subset chain for different kinds of neighborhoods of a vertex. (Contributed by AV, 16-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒} & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → ((𝐺 NeighbVtx 𝑁) ⊆ 𝑆 ∧ 𝑆 ⊆ (𝐺 ClNeighbVtx 𝑁))) | ||
| Theorem | dfvopnbgr2 47839* | Alternate definition of the semiopen neighborhood of a vertex breaking up the subset relationship of an unordered pair. A semiopen neighborhood 𝑈 of a vertex 𝑁 is its open neighborhood together with itself if there is a loop at this vertex. (Contributed by AV, 15-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))} ⇒ ⊢ (𝑁 ∈ 𝑉 → 𝑈 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛}))}) | ||
| Theorem | vopnbgrel 47840* | Characterization of a member 𝑋 of the semiopen neighborhood of a vertex 𝑁 in a graph 𝐺. (Contributed by AV, 16-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))} ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑒 ∈ 𝐸 ((𝑋 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑋 ∈ 𝑒) ∨ (𝑋 = 𝑁 ∧ 𝑒 = {𝑋}))))) | ||
| Theorem | vopnbgrelself 47841* | A vertex 𝑁 is a member of its semiopen neighborhood iff there is a loop joining the vertex with itself. (Contributed by AV, 16-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))} ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝑁 ∈ 𝑈 ↔ ∃𝑒 ∈ 𝐸 𝑒 = {𝑁})) | ||
| Theorem | dfclnbgr6 47842* | Alternate definition of the closed neighborhood of a vertex as union of the vertex with its semiopen neighborhood. (Contributed by AV, 17-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))} ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ 𝑈)) | ||
| Theorem | dfnbgr6 47843* | Alternate definition of the (open) neighborhood of a vertex as a difference of its semiopen neighborhood and the singleton of itself. (Contributed by AV, 17-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))} ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐺 NeighbVtx 𝑁) = (𝑈 ∖ {𝑁})) | ||
| Theorem | dfsclnbgr6 47844* | Alternate definition of a semiclosed neighborhood of a vertex as a union of a semiopen neighborhood and the vertex itself if there is a loop at this vertex. (Contributed by AV, 17-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))} & ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒} ⇒ ⊢ (𝑁 ∈ 𝑉 → 𝑆 = (𝑈 ∪ {𝑛 ∈ {𝑁} ∣ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒})) | ||
| Theorem | dfnbgrss2 47845* | Subset chain for different kinds of neighborhoods of a vertex. (Contributed by AV, 16-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))} & ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒} ⇒ ⊢ (𝑁 ∈ 𝑉 → ((𝐺 NeighbVtx 𝑁) ⊆ 𝑈 ∧ 𝑈 ⊆ 𝑆 ∧ 𝑆 ⊆ (𝐺 ClNeighbVtx 𝑁))) | ||
| Syntax | cisubgr 47846 | Extend class notation with induced subgraphs. |
| class ISubGr | ||
| Definition | df-isubgr 47847* | Define the function mapping graphs and subsets of their vertices to their induced subgraphs. A subgraph induced by a subset of vertices of a graph is a subgraph of the graph which contains all edges of the graph that join vertices of the subgraph (see section I.1 in [Bollobas] p. 2 or section 1.1 in [Diestel] p. 4). Although a graph may be given in any meaningful representation, its induced subgraphs are always ordered pairs of vertices and edges. (Contributed by AV, 27-Apr-2025.) |
| ⊢ ISubGr = (𝑔 ∈ V, 𝑣 ∈ 𝒫 (Vtx‘𝑔) ↦ 〈𝑣, ⦋(iEdg‘𝑔) / 𝑒⦌(𝑒 ↾ {𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) ⊆ 𝑣})〉) | ||
| Theorem | isisubgr 47848* | The subgraph induced by a subset of vertices. (Contributed by AV, 12-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) = 〈𝑆, (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) ⊆ 𝑆})〉) | ||
| Theorem | isubgriedg 47849* | The edges of an induced subgraph. (Contributed by AV, 12-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉) → (iEdg‘(𝐺 ISubGr 𝑆)) = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) ⊆ 𝑆})) | ||
| Theorem | isubgrvtxuhgr 47850 | The subgraph induced by the full set of vertices of a hypergraph. (Contributed by AV, 12-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UHGraph → (𝐺 ISubGr 𝑉) = 〈𝑉, 𝐸〉) | ||
| Theorem | isubgredgss 47851 | The edges of an induced subgraph of a graph are edges of the graph. (Contributed by AV, 24-Sep-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐻 = (𝐺 ISubGr 𝑆) & ⊢ 𝐼 = (Edg‘𝐻) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉) → 𝐼 ⊆ 𝐸) | ||
| Theorem | isubgredg 47852 | 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.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐻 = (𝐺 ISubGr 𝑆) & ⊢ 𝐼 = (Edg‘𝐻) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (𝐾 ∈ 𝐼 ↔ (𝐾 ∈ 𝐸 ∧ 𝐾 ⊆ 𝑆))) | ||
| Theorem | isubgrvtx 47853 | The vertices of an induced subgraph. (Contributed by AV, 12-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉) → (Vtx‘(𝐺 ISubGr 𝑆)) = 𝑆) | ||
| Theorem | isubgruhgr 47854 | An induced subgraph of a hypergraph is a hypergraph. (Contributed by AV, 13-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ UHGraph) | ||
| Theorem | isubgrsubgr 47855 | An induced subgraph of a hypergraph is a subgraph of the hypergraph. (Contributed by AV, 14-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) SubGraph 𝐺) | ||
| Theorem | isubgrupgr 47856 | An induced subgraph of a pseudograph is a pseudograph. (Contributed by AV, 14-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ UPGraph) | ||
| Theorem | isubgrumgr 47857 | An induced subgraph of a multigraph is a multigraph. (Contributed by AV, 15-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ UMGraph) | ||
| Theorem | isubgrusgr 47858 | An induced subgraph of a simple graph is a simple graph. (Contributed by AV, 15-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑆 ⊆ 𝑉) → (𝐺 ISubGr 𝑆) ∈ USGraph) | ||
| Theorem | isubgr0uhgr 47859 | The subgraph induced by an empty set of vertices of a hypergraph. (Contributed by AV, 13-May-2025.) |
| ⊢ (𝐺 ∈ UHGraph → (𝐺 ISubGr ∅) = 〈∅, ∅〉) | ||
This section is about isomorphisms of graphs, whereby the term "isomorphism" is used in both of its meanings (according to the Meriam-Webster dictionary, see https://www.merriam-webster.com/dictionary/isomorphism): "1: the quality or state of being isomorphic." and "2: a one-to-one correspondence between two mathematical sets". At first, an operation GraphIso is defined (see df-grim 47864) which provides the graph isomorphisms (as "one-to-one correspondence") between two given graphs. This definition, however, is applicable for any two sets, but is meaningful only if these sets have "vertices" and "edges". Afterwards, a binary relation ≃𝑔𝑟 is defined (see df-gric 47867) which is true for two graphs iff there is a graph isomorphisms between these graphs. Then these graphs are called "isomorphic". Therefore, this relation is also called "is isomorphic to" relation. More formally, 𝐴 ≃𝑔𝑟 𝐵 ↔ ∃𝑓𝑓 ∈ (𝐴 GraphIso 𝐵) resp. 𝐴 ≃𝑔𝑟 𝐵 ↔ (𝐴 GraphIso 𝐵) ≠ ∅. Notice that there can be multiple isomorphisms between two graphs. For example, let 〈{𝐴, 𝐵}, {{𝐴, 𝐵}}〉 and 〈{{𝑀, 𝑁}, {{𝑀, 𝑁}}〉 be two graphs with two vertices and one edge, then 𝐴 ↦ 𝑀, 𝐵 ↦ 𝑁 and 𝐴 ↦ 𝑁, 𝐵 ↦ 𝑀 are two different isomorphisms between these graphs. The names and symbols are chosen analogously to group isomorphisms GrpIso (see df-gim 19277) resp. isomorphism between groups ≃𝑔 (see df-gic 19278). The general definition of graph isomorphisms and the relation "is isomorphic to" for graphs is specialized for simple hypergraphs (gricushgr 47886) and simple pseudographs (gricuspgr 47887). The latter corresponds to the definition in [Bollobas] p. 3. It is shown that the relation "is isomorphic to" for graphs is an equivalence relation, see gricer 47893. Finally, isomorphic graphs with different representations are studied (opstrgric 47895, ushggricedg 47896). Another approach could be to define a category of graphs (there are maybe multiple ones), where graph morphisms are couples consisting of a function on vertices and a function on edges with required compatibilities, as used in the definition of GraphIso. And then, a graph isomorphism is defined as an isomorphism in the category of graphs (something like "GraphIsom = ( Iso ` GraphCat )" ). Then general category theory theorems could be used, e.g., to show that graph isomorphism is an equivalence relation. | ||
| Syntax | cgrisom 47860 | Extend class notation to include the graph ispmorphisms as pair. |
| class GraphIsom | ||
| Syntax | cgrim 47861 | Extend class notation to include the graph ispmorphisms. |
| class GraphIso | ||
| Syntax | cgric 47862 | Extend class notation to include the "is isomorphic to" relation for graphs. |
| class ≃𝑔𝑟 | ||
| Definition | df-grisom 47863* |
Define the class of all isomorphisms between two graphs. In contrast to
(𝐹
GraphIso 𝐻), which
is a set of functions between the vertices,
(𝐹
GraphIsom 𝐻) is a
set of pairs of functions: a function between
the vertices, and a function between the (indices of the) edges.
It is not clear if such a definition is useful. In the definition by [Diestel] p. 3, for example, the bijection between the vertices is called an isomorphism, as formalized in df-grim 47864. (Contributed by AV, 11-Dec-2022.) (New usage is discouraged.) |
| ⊢ GraphIsom = (𝑥 ∈ V, 𝑦 ∈ V ↦ {〈𝑓, 𝑔〉 ∣ (𝑓:(Vtx‘𝑥)–1-1-onto→(Vtx‘𝑦) ∧ 𝑔:dom (iEdg‘𝑥)–1-1-onto→dom (iEdg‘𝑦) ∧ ∀𝑖 ∈ dom (iEdg‘𝑥)(𝑓 “ ((iEdg‘𝑥)‘𝑖)) = ((iEdg‘𝑦)‘(𝑔‘𝑖)))}) | ||
| Definition | df-grim 47864* | An isomorphism between two graphs is a bijection between the sets of vertices of the two graphs that preserves adjacency, see definition in [Diestel] p. 3. (Contributed by AV, 19-Apr-2025.) |
| ⊢ GraphIso = (𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ∧ ∃𝑗[(iEdg‘𝑔) / 𝑒][(iEdg‘ℎ) / 𝑑](𝑗:dom 𝑒–1-1-onto→dom 𝑑 ∧ ∀𝑖 ∈ dom 𝑒(𝑑‘(𝑗‘𝑖)) = (𝑓 “ (𝑒‘𝑖))))}) | ||
| Theorem | grimfn 47865 | The graph isomorphism function is a well-defined function. (Contributed by AV, 28-Apr-2025.) |
| ⊢ GraphIso Fn (V × V) | ||
| Theorem | grimdmrel 47866 | The domain of the graph isomorphism function is a relation. (Contributed by AV, 28-Apr-2025.) |
| ⊢ Rel dom GraphIso | ||
| Definition | df-gric 47867 | Two graphs are said to be isomorphic iff they are connected by at least one isomorphism, see definition in [Diestel] p. 3 and definition in [Bollobas] p. 3. Isomorphic graphs share all global graph properties like order and size. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 19-Apr-2025.) |
| ⊢ ≃𝑔𝑟 = (◡ GraphIso “ (V ∖ 1o)) | ||
| Theorem | isgrim 47868* | An isomorphism of graphs is a bijection between their vertices that preserves adjacency. (Contributed by AV, 19-Apr-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐷 = (iEdg‘𝐻) ⇒ ⊢ ((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∃𝑗(𝑗:dom 𝐸–1-1-onto→dom 𝐷 ∧ ∀𝑖 ∈ dom 𝐸(𝐷‘(𝑗‘𝑖)) = (𝐹 “ (𝐸‘𝑖)))))) | ||
| Theorem | grimprop 47869* | Properties of an isomorphism of graphs. (Contributed by AV, 29-Apr-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐷 = (iEdg‘𝐻) ⇒ ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∃𝑗(𝑗:dom 𝐸–1-1-onto→dom 𝐷 ∧ ∀𝑖 ∈ dom 𝐸(𝐷‘(𝑗‘𝑖)) = (𝐹 “ (𝐸‘𝑖))))) | ||
| Theorem | grimf1o 47870 | An isomorphism of graphs is a bijection between their vertices. (Contributed by AV, 29-Apr-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) ⇒ ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:𝑉–1-1-onto→𝑊) | ||
| Theorem | isuspgrim0lem 47871* | An isomorphism of simple pseudographs is a bijection between their vertices which induces a bijection between their edges. (Contributed by AV, 21-Apr-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (Edg‘𝐻) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐽 = (iEdg‘𝐻) & ⊢ 𝑀 = (𝑥 ∈ 𝐸 ↦ (𝐹 “ 𝑥)) & ⊢ 𝑁 = (𝑥 ∈ dom 𝐼 ↦ (◡𝐽‘(𝑀‘(𝐼‘𝑥)))) ⇒ ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ 𝑀:𝐸–1-1-onto→𝐷) → (𝑁:dom 𝐼–1-1-onto→dom 𝐽 ∧ ∀𝑖 ∈ dom 𝐼(𝐽‘(𝑁‘𝑖)) = (𝐹 “ (𝐼‘𝑖)))) | ||
| Theorem | isuspgrim0 47872* | An isomorphism of simple pseudographs is a bijection between their vertices which induces a bijection between their edges. (Contributed by AV, 21-Apr-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (Edg‘𝐻) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷))) | ||
| Theorem | uspgrimprop 47873* | An isomorphism of simple pseudographs is a bijection between their vertices that preserves adjacency, i.e. there is an edge in one graph connecting one or two vertices iff there is an edge in the other graph connecting the vertices which are the images of the vertices. (Contributed by AV, 27-Apr-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (Edg‘𝐻) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (𝐹 ∈ (𝐺 GraphIso 𝐻) → (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷)))) | ||
| Theorem | isuspgrimlem 47874* | Lemma for isuspgrim 47875. (Contributed by AV, 27-Apr-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (Edg‘𝐻) ⇒ ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷)) → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷) | ||
| Theorem | isuspgrim 47875* | A class is an isomorphism of simple pseudographs iff it is a bijection between their vertices that preserves adjacency, i.e. there is an edge in one graph connecting one or two vertices iff there is an edge in the other graph connecting the vertices which are the images of the vertices. This corresponds to the formal definition in [Bollobas] p. 3 and the definition in [Diestel] p. 3. (Contributed by AV, 27-Apr-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (Edg‘𝐻) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷)))) | ||
| Theorem | grimidvtxedg 47876 | The identity relation restricted to the set of vertices of a graph is a graph isomorphism between the graph and a graph with the same vertices and edges. (Contributed by AV, 4-May-2025.) |
| ⊢ (𝜑 → 𝐺 ∈ UHGraph) & ⊢ (𝜑 → 𝐻 ∈ 𝑉) & ⊢ (𝜑 → (Vtx‘𝐺) = (Vtx‘𝐻)) & ⊢ (𝜑 → (iEdg‘𝐺) = (iEdg‘𝐻)) ⇒ ⊢ (𝜑 → ( I ↾ (Vtx‘𝐺)) ∈ (𝐺 GraphIso 𝐻)) | ||
| Theorem | grimid 47877 | The identity relation restricted to the set of vertices of a graph is a graph isomorphism between the graph and itself. (Contributed by AV, 29-Apr-2025.) (Prove shortened by AV, 5-May-2025.) |
| ⊢ (𝐺 ∈ UHGraph → ( I ↾ (Vtx‘𝐺)) ∈ (𝐺 GraphIso 𝐺)) | ||
| Theorem | grimuhgr 47878 | If there is a graph isomorphism between a hypergraph and a class with an edge function, the class is also a hypergraph. (Contributed by AV, 2-May-2025.) |
| ⊢ ((𝑆 ∈ UHGraph ∧ 𝐹 ∈ (𝑆 GraphIso 𝑇) ∧ Fun (iEdg‘𝑇)) → 𝑇 ∈ UHGraph) | ||
| Theorem | grimcnv 47879 | The converse of a graph isomorphism is a graph isomorphism. (Contributed by AV, 1-May-2025.) |
| ⊢ (𝑆 ∈ UHGraph → (𝐹 ∈ (𝑆 GraphIso 𝑇) → ◡𝐹 ∈ (𝑇 GraphIso 𝑆))) | ||
| Theorem | grimco 47880 | The composition of graph isomorphisms is a graph isomorphism. (Contributed by AV, 3-May-2025.) |
| ⊢ ((𝐹 ∈ (𝑇 GraphIso 𝑈) ∧ 𝐺 ∈ (𝑆 GraphIso 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GraphIso 𝑈)) | ||
| Theorem | brgric 47881 | The relation "is isomorphic to" for graphs. (Contributed by AV, 28-Apr-2025.) |
| ⊢ (𝑅 ≃𝑔𝑟 𝑆 ↔ (𝑅 GraphIso 𝑆) ≠ ∅) | ||
| Theorem | brgrici 47882 | Prove that two graphs are isomorphic by an explicit isomorphism. (Contributed by AV, 28-Apr-2025.) |
| ⊢ (𝐹 ∈ (𝑅 GraphIso 𝑆) → 𝑅 ≃𝑔𝑟 𝑆) | ||
| Theorem | gricrcl 47883 | Reverse closure of the "is isomorphic to" relation for graphs. (Contributed by AV, 12-Jun-2025.) |
| ⊢ (𝐺 ≃𝑔𝑟 𝑆 → (𝐺 ∈ V ∧ 𝑆 ∈ V)) | ||
| Theorem | dfgric2 47884* | Alternate, explicit definition of the "is isomorphic to" relation for two graphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 5-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐴) & ⊢ 𝑊 = (Vtx‘𝐵) & ⊢ 𝐼 = (iEdg‘𝐴) & ⊢ 𝐽 = (iEdg‘𝐵) ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐴 ≃𝑔𝑟 𝐵 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃𝑔(𝑔:dom 𝐼–1-1-onto→dom 𝐽 ∧ ∀𝑖 ∈ dom 𝐼(𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))))) | ||
| Theorem | gricbri 47885* | Implications of two graphs being isomorphic. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 5-May-2025.) (Proof shortened by AV, 12-Jun-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐴) & ⊢ 𝑊 = (Vtx‘𝐵) & ⊢ 𝐼 = (iEdg‘𝐴) & ⊢ 𝐽 = (iEdg‘𝐵) ⇒ ⊢ (𝐴 ≃𝑔𝑟 𝐵 → ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃𝑔(𝑔:dom 𝐼–1-1-onto→dom 𝐽 ∧ ∀𝑖 ∈ dom 𝐼(𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖))))) | ||
| Theorem | gricushgr 47886* | The "is isomorphic to" relation for two simple hypergraphs. (Contributed by AV, 28-Nov-2022.) |
| ⊢ 𝑉 = (Vtx‘𝐴) & ⊢ 𝑊 = (Vtx‘𝐵) & ⊢ 𝐸 = (Edg‘𝐴) & ⊢ 𝐾 = (Edg‘𝐵) ⇒ ⊢ ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (𝐴 ≃𝑔𝑟 𝐵 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))))) | ||
| Theorem | gricuspgr 47887* | The "is isomorphic to" relation for two simple pseudographs. This corresponds to the definition in [Bollobas] p. 3. (Contributed by AV, 1-Dec-2022.) (Proof shortened by AV, 5-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐴) & ⊢ 𝑊 = (Vtx‘𝐵) & ⊢ 𝐸 = (Edg‘𝐴) & ⊢ 𝐾 = (Edg‘𝐵) ⇒ ⊢ ((𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph) → (𝐴 ≃𝑔𝑟 𝐵 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑓‘𝑎), (𝑓‘𝑏)} ∈ 𝐾)))) | ||
| Theorem | gricrel 47888 | The "is isomorphic to" relation for graphs is a relation. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 5-May-2025.) |
| ⊢ Rel ≃𝑔𝑟 | ||
| Theorem | gricref 47889 | Graph isomorphism is reflexive for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 29-Apr-2025.) |
| ⊢ (𝐺 ∈ UHGraph → 𝐺 ≃𝑔𝑟 𝐺) | ||
| Theorem | gricsym 47890 | Graph isomorphism is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 3-May-2025.) |
| ⊢ (𝐺 ∈ UHGraph → (𝐺 ≃𝑔𝑟 𝑆 → 𝑆 ≃𝑔𝑟 𝐺)) | ||
| Theorem | gricsymb 47891 | Graph isomorphism is symmetric in both directions for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Proof shortened by AV, 3-May-2025.) |
| ⊢ ((𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph) → (𝐴 ≃𝑔𝑟 𝐵 ↔ 𝐵 ≃𝑔𝑟 𝐴)) | ||
| Theorem | grictr 47892 | Graph isomorphism is transitive. (Contributed by AV, 5-Dec-2022.) (Revised by AV, 3-May-2025.) |
| ⊢ ((𝑅 ≃𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑔𝑟 𝑇) → 𝑅 ≃𝑔𝑟 𝑇) | ||
| Theorem | gricer 47893 | Isomorphism is an equivalence relation on hypergraphs. (Contributed by AV, 3-May-2025.) (Proof shortened by AV, 11-Jul-2025.) |
| ⊢ ( ≃𝑔𝑟 ∩ (UHGraph × UHGraph)) Er UHGraph | ||
| Theorem | gricen 47894 | Isomorphic graphs have equinumerous sets of vertices. (Contributed by AV, 3-May-2025.) |
| ⊢ 𝐵 = (Vtx‘𝑅) & ⊢ 𝐶 = (Vtx‘𝑆) ⇒ ⊢ (𝑅 ≃𝑔𝑟 𝑆 → 𝐵 ≈ 𝐶) | ||
| Theorem | opstrgric 47895 | A graph represented as an extensible structure with vertices as base set and indexed edges is isomorphic to a hypergraph represented as ordered pair with the same vertices and edges. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 4-May-2025.) |
| ⊢ 𝐺 = 〈𝑉, 𝐸〉 & ⊢ 𝐻 = {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 𝐺 ≃𝑔𝑟 𝐻) | ||
| Theorem | ushggricedg 47896 | A simple hypergraph (with arbitrarily indexed edges) is isomorphic to a graph with the same vertices and the same edges, indexed by the edges themselves. (Contributed by AV, 11-Nov-2022.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐻 = 〈𝑉, ( I ↾ 𝐸)〉 ⇒ ⊢ (𝐺 ∈ USHGraph → 𝐺 ≃𝑔𝑟 𝐻) | ||
| Theorem | isubgrgrim 47897* | Isomorphic subgraphs induced by subsets of vertices of two graphs. (Contributed by AV, 29-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐽 = (iEdg‘𝐻) & ⊢ 𝐾 = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) ⊆ 𝑁} & ⊢ 𝐿 = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) ⊆ 𝑀} ⇒ ⊢ (((𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇) ∧ (𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊)) → ((𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr 𝑀) ↔ ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))))) | ||
| Theorem | uhgrimisgrgriclem 47898* | Lemma for uhgrimisgrgric 47899. (Contributed by AV, 31-May-2025.) |
| ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) ↔ ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽))) | ||
| Theorem | uhgrimisgrgric 47899 | For isomorphic hypergraphs, the induced subgraph of a subset of vertices of one graph is isomorphic to the subgraph induced by the image of the subset. (Contributed by AV, 31-May-2025.) |
| ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻) ∧ 𝑁 ⊆ 𝑉) → (𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr (𝐹 “ 𝑁))) | ||
| Theorem | clnbgrisubgrgrim 47900* | Isomorphic subgraphs induced by closed neighborhoods of vertices of two graphs. (Contributed by AV, 29-May-2025.) |
| ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐽 = (iEdg‘𝐻) & ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝑀 = (𝐻 ClNeighbVtx 𝑌) & ⊢ 𝐾 = {𝑥 ∈ dom 𝐼 ∣ (𝐼‘𝑥) ⊆ 𝑁} & ⊢ 𝐿 = {𝑥 ∈ dom 𝐽 ∣ (𝐽‘𝑥) ⊆ 𝑀} ⇒ ⊢ ((𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇) → ((𝐺 ISubGr 𝑁) ≃𝑔𝑟 (𝐻 ISubGr 𝑀) ↔ ∃𝑓(𝑓:𝑁–1-1-onto→𝑀 ∧ ∃𝑔(𝑔:𝐾–1-1-onto→𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |