![]() |
Metamath
Proof Explorer Theorem List (p. 479 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-grim 47801* | 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 47802 | The graph isomorphism function is a well-defined function. (Contributed by AV, 28-Apr-2025.) |
⊢ GraphIso Fn (V × V) | ||
Theorem | grimdmrel 47803 | The domain of the graph isomorphism function is a relation. (Contributed by AV, 28-Apr-2025.) |
⊢ Rel dom GraphIso | ||
Definition | df-gric 47804 | 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 47805* | 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 47806* | 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 47807 | An isomorphism of graphs is a bijection between their vertices. (Contributed by AV, 29-Apr-2025.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) ⇒ ⊢ (𝐹 ∈ (𝐺 GraphIso 𝐻) → 𝐹:𝑉–1-1-onto→𝑊) | ||
Theorem | isuspgrim0lem 47808* | 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 47809* | 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 47810* | 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 47811* | Lemma for isuspgrim 47812. (Contributed by AV, 27-Apr-2025.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (Edg‘𝐻) ⇒ ⊢ ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph) ∧ 𝐹:𝑉–1-1-onto→𝑊) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 ({𝑥, 𝑦} ∈ 𝐸 ↔ {(𝐹‘𝑥), (𝐹‘𝑦)} ∈ 𝐷)) → (𝑒 ∈ 𝐸 ↦ (𝐹 “ 𝑒)):𝐸–1-1-onto→𝐷) | ||
Theorem | isuspgrim 47812* | 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 47813 | 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 47814 | 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 47815 | 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 47816 | The converse of a graph isomorphism is a graph isomorphism. (Contributed by AV, 1-May-2025.) |
⊢ (𝑆 ∈ UHGraph → (𝐹 ∈ (𝑆 GraphIso 𝑇) → ◡𝐹 ∈ (𝑇 GraphIso 𝑆))) | ||
Theorem | grimco 47817 | The composition of graph isomorphisms is a graph isomorphism. (Contributed by AV, 3-May-2025.) |
⊢ ((𝐹 ∈ (𝑇 GraphIso 𝑈) ∧ 𝐺 ∈ (𝑆 GraphIso 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GraphIso 𝑈)) | ||
Theorem | brgric 47818 | The relation "is isomorphic to" for graphs. (Contributed by AV, 28-Apr-2025.) |
⊢ (𝑅 ≃𝑔𝑟 𝑆 ↔ (𝑅 GraphIso 𝑆) ≠ ∅) | ||
Theorem | brgrici 47819 | Prove that two graphs are isomorphic by an explicit isomorphism. (Contributed by AV, 28-Apr-2025.) |
⊢ (𝐹 ∈ (𝑅 GraphIso 𝑆) → 𝑅 ≃𝑔𝑟 𝑆) | ||
Theorem | gricrcl 47820 | Reverse closure of the "is isomorphic to" relation for graphs. (Contributed by AV, 12-Jun-2025.) |
⊢ (𝐺 ≃𝑔𝑟 𝑆 → (𝐺 ∈ V ∧ 𝑆 ∈ V)) | ||
Theorem | dfgric2 47821* | 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 47822* | 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 47823* | 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 47824* | 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 47825 | 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 47826 | Graph isomorphism is reflexive for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 29-Apr-2025.) |
⊢ (𝐺 ∈ UHGraph → 𝐺 ≃𝑔𝑟 𝐺) | ||
Theorem | gricsym 47827 | Graph isomorphism is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022.) (Revised by AV, 3-May-2025.) |
⊢ (𝐺 ∈ UHGraph → (𝐺 ≃𝑔𝑟 𝑆 → 𝑆 ≃𝑔𝑟 𝐺)) | ||
Theorem | gricsymb 47828 | 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 47829 | Graph isomorphism is transitive. (Contributed by AV, 5-Dec-2022.) (Revised by AV, 3-May-2025.) |
⊢ ((𝑅 ≃𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑔𝑟 𝑇) → 𝑅 ≃𝑔𝑟 𝑇) | ||
Theorem | gricer 47830 | 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 47831 | Isomorphic graphs have equinumerous sets of vertices. (Contributed by AV, 3-May-2025.) |
⊢ 𝐵 = (Vtx‘𝑅) & ⊢ 𝐶 = (Vtx‘𝑆) ⇒ ⊢ (𝑅 ≃𝑔𝑟 𝑆 → 𝐵 ≈ 𝐶) | ||
Theorem | opstrgric 47832 | 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 47833 | 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 47834* | 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 47835* | Lemma for uhgrimisgrgric 47836. (Contributed by AV, 31-May-2025.) |
⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) ↔ ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽))) | ||
Theorem | uhgrimisgrgric 47836 | 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 47837* | 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→𝐿 ∧ ∀𝑖 ∈ 𝐾 (𝑓 “ (𝐼‘𝑖)) = (𝐽‘(𝑔‘𝑖)))))) | ||
Theorem | clnbgrgrimlem 47838* | Lemma for clnbgrgrim 47839: 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 47839 | Graph isomorphisms between hypergraphs map closed neighborhoods onto closed neighborhoods. (Contributed by AV, 2-Jun-2025.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph) ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) ∧ 𝑋 ∈ 𝑉) → (𝐻 ClNeighbVtx (𝐹‘𝑋)) = (𝐹 “ (𝐺 ClNeighbVtx 𝑋))) | ||
Theorem | grimedg 47840 | 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 47842 is designed for a special purpose, namely to provide a criterion for two graphs being not isomorphic (see grimgrtri 47851). 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 47842 may become obsolete. | ||
Syntax | cgrtri 47841 | Extend class notation with triangles (in a graph). |
class GrTriangles | ||
Definition | df-grtri 47842* | 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 47849. (TODO: and a cycle of length 3 ,see grtricycl ). (Contributed by AV, 20-Jul-2025.) |
⊢ GrTriangles = (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(Edg‘𝑔) / 𝑒⦌{𝑡 ∈ 𝒫 𝑣 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))}) | ||
Theorem | grtriproplem 47843 | Lemma for grtriprop 47845. (Contributed by AV, 23-Jul-2025.) |
⊢ ((𝑓:(0..^3)–1-1-onto→{𝑥, 𝑦, 𝑧} ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝐸 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝐸 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝐸)) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) | ||
Theorem | grtri 47844* | 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 47845* | The properties of a triangle. (Contributed by AV, 25-Jul-2025.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑇 ∈ (GrTriangles‘𝐺) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑇 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑇) = 3 ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))) | ||
Theorem | grtrif1o 47846 | 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 47847* | A triangle in a graph. (Contributed by AV, 20-Jul-2025.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑇 ∈ (GrTriangles‘𝐺) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑇 = {𝑥, 𝑦, 𝑧} ∧ (♯‘𝑇) = 3 ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑥, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))) | ||
Theorem | grtrissvtx 47848 | A triangle is a subset of the vertices (of a graph). (Contributed by AV, 26-Jul-2025.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑇 ∈ (GrTriangles‘𝐺) → 𝑇 ⊆ 𝑉) | ||
Theorem | grtriclwlk3 47849 | A triangle induces a closed walk of length 3 . (Contributed by AV, 26-Jul-2025.) |
⊢ (𝜑 → 𝑇 ∈ (GrTriangles‘𝐺)) & ⊢ (𝜑 → 𝑃:(0..^3)–1-1-onto→𝑇) ⇒ ⊢ (𝜑 → 𝑃 ∈ (3 ClWWalksN 𝐺)) | ||
Theorem | grtrimap 47850 | Conditions for mapping triangles onto triangles. Lemma for grimgrtri 47851 and grlimgrtri 47898. (Contributed by AV, 23-Aug-2025.) |
⊢ (𝐹:𝑉–1-1→𝑊 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑇 = {𝑎, 𝑏, 𝑐} ∧ (♯‘𝑇) = 3)) → (((𝐹‘𝑎) ∈ 𝑊 ∧ (𝐹‘𝑏) ∈ 𝑊 ∧ (𝐹‘𝑐) ∈ 𝑊) ∧ (𝐹 “ 𝑇) = {(𝐹‘𝑎), (𝐹‘𝑏), (𝐹‘𝑐)} ∧ (♯‘(𝐹 “ 𝑇)) = 3))) | ||
Theorem | grimgrtri 47851 | 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 47852* | 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 47853 | Extend class notation with star graphs. |
class StarGr | ||
Definition | df-stgr 47854* | 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 47862, (StarGr‘1) will be a single edge (graph with two vertices connected by an edge), see stgr1 47863, 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 47855* | The star graph SN. (Contributed by AV, 10-Sep-2025.) |
⊢ (𝑁 ∈ ℕ0 → (StarGr‘𝑁) = {〈(Base‘ndx), (0...𝑁)〉, 〈(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})〉}) | ||
Theorem | stgrvtx 47856 | The vertices of the star graph SN. (Contributed by AV, 11-Sep-2025.) |
⊢ (𝑁 ∈ ℕ0 → (Vtx‘(StarGr‘𝑁)) = (0...𝑁)) | ||
Theorem | stgriedg 47857* | The indexed edges of the star graph SN. (Contributed by AV, 11-Sep-2025.) |
⊢ (𝑁 ∈ ℕ0 → (iEdg‘(StarGr‘𝑁)) = ( I ↾ {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}})) | ||
Theorem | stgredg 47858* | The edges of the star graph SN. (Contributed by AV, 11-Sep-2025.) |
⊢ (𝑁 ∈ ℕ0 → (Edg‘(StarGr‘𝑁)) = {𝑒 ∈ 𝒫 (0...𝑁) ∣ ∃𝑥 ∈ (1...𝑁)𝑒 = {0, 𝑥}}) | ||
Theorem | stgredgel 47859* | An edge of the star graph SN. (Contributed by AV, 11-Sep-2025.) |
⊢ (𝑁 ∈ ℕ0 → (𝐸 ∈ (Edg‘(StarGr‘𝑁)) ↔ (𝐸 ⊆ (0...𝑁) ∧ ∃𝑥 ∈ (1...𝑁)𝐸 = {0, 𝑥}))) | ||
Theorem | stgredgiun 47860* | The edges of the star graph SN as indexed union. (Contributed by AV, 29-Sep-2025.) |
⊢ (𝑁 ∈ ℕ0 → (Edg‘(StarGr‘𝑁)) = ∪ 𝑥 ∈ (1...𝑁){{0, 𝑥}}) | ||
Theorem | stgrusgra 47861 | The star graph SN is a simple graph. (Contributed by AV, 11-Sep-2025.) |
⊢ (𝑁 ∈ ℕ0 → (StarGr‘𝑁) ∈ USGraph) | ||
Theorem | stgr0 47862 | 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 47863 | 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 47864 | The center ("internal node") of a star graph SN. (Contributed by AV, 12-Sep-2025.) |
⊢ 𝐺 = (StarGr‘𝑁) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ ℕ0 → 0 ∈ 𝑉) | ||
Theorem | stgrorder 47865 | The order of a star graph SN. (Contributed by AV, 12-Sep-2025.) |
⊢ 𝐺 = (StarGr‘𝑁) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ ℕ0 → (♯‘𝑉) = (𝑁 + 1)) | ||
Theorem | stgrnbgr0 47866 | 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 47867 | 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 47868 | Lemma 1 for isubgr3stgr 47877. (Contributed by AV, 16-Sep-2025.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝐹 = (𝐻 ∪ {〈𝑋, 𝑌〉}) ⇒ ⊢ ((𝐻:𝑈–1-1-onto→𝑅 ∧ 𝑋 ∈ 𝑉 ∧ (𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅)) → 𝐹:𝐶–1-1-onto→(𝑅 ∪ {𝑌})) | ||
Theorem | isubgr3stgrlem2 47869* | Lemma 2 for isubgr3stgr 47877. (Contributed by AV, 16-Sep-2025.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑆 = (StarGr‘𝑁) & ⊢ 𝑊 = (Vtx‘𝑆) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ∃𝑓 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0})) | ||
Theorem | isubgr3stgrlem3 47870* | Lemma 3 for isubgr3stgr 47877. (Contributed by AV, 17-Sep-2025.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑆 = (StarGr‘𝑁) & ⊢ 𝑊 = (Vtx‘𝑆) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ∃𝑔(𝑔:𝐶–1-1-onto→𝑊 ∧ (𝑔‘𝑋) = 0)) | ||
Theorem | isubgr3stgrlem4 47871* | Lemma 4 for isubgr3stgr 47877. (Contributed by AV, 24-Sep-2025.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑆 = (StarGr‘𝑁) & ⊢ 𝑊 = (Vtx‘𝑆) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐴 = 𝑋 ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ∃𝑧 ∈ (1...𝑁)(𝐹 “ {𝐴, 𝐵}) = {0, 𝑧}) | ||
Theorem | isubgr3stgrlem5 47872* | Lemma 5 for isubgr3stgr 47877. (Contributed by AV, 24-Sep-2025.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑆 = (StarGr‘𝑁) & ⊢ 𝑊 = (Vtx‘𝑆) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶)) & ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖)) ⇒ ⊢ ((𝐹:𝐶⟶𝑊 ∧ 𝑌 ∈ 𝐼) → (𝐻‘𝑌) = (𝐹 “ 𝑌)) | ||
Theorem | isubgr3stgrlem6 47873* | Lemma 6 for isubgr3stgr 47877. (Contributed by AV, 24-Sep-2025.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑆 = (StarGr‘𝑁) & ⊢ 𝑊 = (Vtx‘𝑆) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶)) & ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖)) ⇒ ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 𝐻:𝐼⟶(Edg‘(StarGr‘𝑁))) | ||
Theorem | isubgr3stgrlem7 47874* | Lemma 7 for isubgr3stgr 47877. (Contributed by AV, 29-Sep-2025.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑆 = (StarGr‘𝑁) & ⊢ 𝑊 = (Vtx‘𝑆) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶)) & ⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖)) ⇒ ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ 𝐽 ∈ (Edg‘(StarGr‘𝑁))) → (◡𝐹 “ 𝐽) ∈ 𝐼) | ||
Theorem | isubgr3stgrlem8 47875* | Lemma 8 for isubgr3stgr 47877. (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 47876* | Lemma 9 for isubgr3stgr 47877. (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 47877* | 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 47889. This definition is according to a chat in mathoverflow (https://mathoverflow.net/questions/491133/locally-isomorphic-graphs 47889): roughly speaking, it restricts the correspondence of two graphs to their neighborhoods. Additionally, a binary relation ≃𝑙𝑔𝑟 is defined (see df-grlic 47883) 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 47911. The names and symbols are chosen analogously to group isomorphisms GrpIso (see df-gim 19289) and graph isomorphisms GraphIso (see df-grim 47801) resp. isomorphism between groups ≃𝑔 (see df-gic 19290) and isomorphism between graphs ≃𝑔𝑟 (see df-gric 47804). In the future, it should be shown that there are local isomorphisms between two graphs which are not (ordinary) isomorphisms between these graphs, as dicussed in the above mentioned chat in mathoverflow. | ||
Syntax | cgrlim 47878 | The class of graph local isomorphism sets. |
class GraphLocIso | ||
Syntax | cgrlic 47879 | The class of the graph local isomorphism relation. |
class ≃𝑙𝑔𝑟 | ||
Definition | df-grlim 47880* | 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 47881 | The graph local isomorphism function is a well-defined function. (Contributed by AV, 20-May-2025.) |
⊢ GraphLocIso Fn (V × V) | ||
Theorem | grlimdmrel 47882 | The domain of the graph local isomorphism function is a relation. (Contributed by AV, 20-May-2025.) |
⊢ Rel dom GraphLocIso | ||
Definition | df-grlic 47883 | 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 47884* | 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 47885* | 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 47886* | 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 47887 | 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 47888* | 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 47889 | An isomorphism of hypergraphs is a local isomorphism between the two graphs. (Contributed by AV, 2-Jun-2025.) |
⊢ ((𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ (𝐺 GraphIso 𝐻)) → 𝐹 ∈ (𝐺 GraphLocIso 𝐻)) | ||
Theorem | uspgrlimlem1 47890* | Lemma 1 for uspgrlim 47894. (Contributed by AV, 16-Aug-2025.) |
⊢ 𝑀 = (𝐻 ClNeighbVtx 𝑋) & ⊢ 𝐽 = (Edg‘𝐻) & ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀} ⇒ ⊢ (𝐻 ∈ USPGraph → 𝐿 = ((iEdg‘𝐻) “ {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀})) | ||
Theorem | uspgrlimlem2 47891* | Lemma 2 for uspgrlim 47894. (Contributed by AV, 16-Aug-2025.) |
⊢ 𝑀 = (𝐻 ClNeighbVtx 𝑋) & ⊢ 𝐽 = (Edg‘𝐻) & ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀} ⇒ ⊢ (𝐻 ∈ USPGraph → (◡(iEdg‘𝐻) “ 𝐿) = {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) ⊆ 𝑀}) | ||
Theorem | uspgrlimlem3 47892* | Lemma 3 for uspgrlim 47894. (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 47893* | Lemma 4 for uspgrlim 47894. (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 47894* | 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 47885). (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 47895* | 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 47896* | Lemma 3 for grlimgrtri 47898. (Contributed by AV, 24-Aug-2025.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑎) & ⊢ 𝐼 = (Edg‘𝐺) & ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁} ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ ({𝑎, 𝑏} ∈ 𝐼 ∧ {𝑎, 𝑐} ∈ 𝐼 ∧ {𝑏, 𝑐} ∈ 𝐼)) → ({𝑎, 𝑏} ∈ 𝐾 ∧ {𝑎, 𝑐} ∈ 𝐾 ∧ {𝑏, 𝑐} ∈ 𝐾)) | ||
Theorem | grlimgrtrilem2 47897* | Lemma 3 for grlimgrtri 47898. (Contributed by AV, 23-Aug-2025.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑎) & ⊢ 𝐼 = (Edg‘𝐺) & ⊢ 𝐾 = {𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁} & ⊢ 𝑀 = (𝐻 ClNeighbVtx (𝐹‘𝑎)) & ⊢ 𝐽 = (Edg‘𝐻) & ⊢ 𝐿 = {𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀} ⇒ ⊢ (((𝑓:𝑁–1-1-onto→𝑀 ∧ 𝑔:𝐾–1-1-onto→𝐿) ∧ ∀𝑖 ∈ 𝐾 (𝑓 “ 𝑖) = (𝑔‘𝑖) ∧ {𝑏, 𝑐} ∈ 𝐾) → {(𝑓‘𝑏), (𝑓‘𝑐)} ∈ 𝐽) | ||
Theorem | grlimgrtri 47898* | Local isomorphisms between simple pseudographs map triangles onto triangles. (Contributed by AV, 24-Aug-2025.) |
⊢ (𝜑 → 𝐺 ∈ USPGraph) & ⊢ (𝜑 → 𝐻 ∈ USPGraph) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 GraphLocIso 𝐻)) & ⊢ (𝜑 → 𝑇 ∈ (GrTriangles‘𝐺)) ⇒ ⊢ (𝜑 → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐻)) | ||
Theorem | brgrlic 47899 | The relation "is locally isomorphic to" for graphs. (Contributed by AV, 9-Jun-2025.) |
⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 ↔ (𝑅 GraphLocIso 𝑆) ≠ ∅) | ||
Theorem | brgrilci 47900 | Prove that two graphs are locally isomorphic by an explicit local isomorphism. (Contributed by AV, 9-Jun-2025.) |
⊢ (𝐹 ∈ (𝑅 GraphLocIso 𝑆) → 𝑅 ≃𝑙𝑔𝑟 𝑆) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |