![]() |
Metamath
Proof Explorer Theorem List (p. 264 of 435) | < 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-28331) |
![]() (28332-29856) |
![]() (29857-43448) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 1vgrex 26301 | A graph with at least one vertex is a set. (Contributed by AV, 2-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → 𝐺 ∈ V) | ||
Theorem | opvtxval 26302 | The set of vertices of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 21-Sep-2020.) |
⊢ (𝐺 ∈ (V × V) → (Vtx‘𝐺) = (1st ‘𝐺)) | ||
Theorem | opvtxfv 26303 | The set of vertices of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 21-Sep-2020.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘〈𝑉, 𝐸〉) = 𝑉) | ||
Theorem | opvtxov 26304 | The set of vertices of a graph represented as an ordered pair of vertices and indexed edges as operation value. (Contributed by AV, 21-Sep-2020.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉Vtx𝐸) = 𝑉) | ||
Theorem | opiedgval 26305 | The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 21-Sep-2020.) |
⊢ (𝐺 ∈ (V × V) → (iEdg‘𝐺) = (2nd ‘𝐺)) | ||
Theorem | opiedgfv 26306 | The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 21-Sep-2020.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘〈𝑉, 𝐸〉) = 𝐸) | ||
Theorem | opiedgov 26307 | The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as operation value. (Contributed by AV, 21-Sep-2020.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉iEdg𝐸) = 𝐸) | ||
Theorem | opvtxfvi 26308 | The set of vertices of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 4-Mar-2021.) |
⊢ 𝑉 ∈ V & ⊢ 𝐸 ∈ V ⇒ ⊢ (Vtx‘〈𝑉, 𝐸〉) = 𝑉 | ||
Theorem | opiedgfvi 26309 | The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 4-Mar-2021.) |
⊢ 𝑉 ∈ V & ⊢ 𝐸 ∈ V ⇒ ⊢ (iEdg‘〈𝑉, 𝐸〉) = 𝐸 | ||
Theorem | funvtxdmge2val 26310 | The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) |
⊢ ((Fun (𝐺 ∖ {∅}) ∧ 2 ≤ (♯‘dom 𝐺)) → (Vtx‘𝐺) = (Base‘𝐺)) | ||
Theorem | funiedgdmge2val 26311 | The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) |
⊢ ((Fun (𝐺 ∖ {∅}) ∧ 2 ≤ (♯‘dom 𝐺)) → (iEdg‘𝐺) = (.ef‘𝐺)) | ||
Theorem | funvtxdm2val 26312 | The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((Fun (𝐺 ∖ {∅}) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵} ⊆ dom 𝐺) → (Vtx‘𝐺) = (Base‘𝐺)) | ||
Theorem | funiedgdm2val 26313 | The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((Fun (𝐺 ∖ {∅}) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵} ⊆ dom 𝐺) → (iEdg‘𝐺) = (.ef‘𝐺)) | ||
Theorem | funvtxval0 26314 | The set of vertices of an extensible structure with a base set and (at least) another slot. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) |
⊢ 𝑆 ∈ V ⇒ ⊢ ((Fun (𝐺 ∖ {∅}) ∧ 𝑆 ≠ (Base‘ndx) ∧ {(Base‘ndx), 𝑆} ⊆ dom 𝐺) → (Vtx‘𝐺) = (Base‘𝐺)) | ||
Theorem | basvtxval 26315 | The set of vertices of a graph represented as an extensible structure with the set of vertices as base set. (Contributed by AV, 14-Oct-2020.) (Revised by AV, 12-Nov-2021.) |
⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → 2 ≤ (♯‘dom 𝐺)) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 〈(Base‘ndx), 𝑉〉 ∈ 𝐺) ⇒ ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) | ||
Theorem | edgfiedgval 26316 | The set of indexed edges of a graph represented as an extensible structure with the indexed edges in the slot for edge functions. (Contributed by AV, 14-Oct-2020.) (Revised by AV, 12-Nov-2021.) |
⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → 2 ≤ (♯‘dom 𝐺)) & ⊢ (𝜑 → 𝐸 ∈ 𝑌) & ⊢ (𝜑 → 〈(.ef‘ndx), 𝐸〉 ∈ 𝐺) ⇒ ⊢ (𝜑 → (iEdg‘𝐺) = 𝐸) | ||
Theorem | funvtxval 26317 | The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) |
⊢ ((Fun (𝐺 ∖ {∅}) ∧ {(Base‘ndx), (.ef‘ndx)} ⊆ dom 𝐺) → (Vtx‘𝐺) = (Base‘𝐺)) | ||
Theorem | funiedgval 26318 | The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 21-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) |
⊢ ((Fun (𝐺 ∖ {∅}) ∧ {(Base‘ndx), (.ef‘ndx)} ⊆ dom 𝐺) → (iEdg‘𝐺) = (.ef‘𝐺)) | ||
Theorem | structvtxvallem 26319 | Lemma for structvtxval 26320 and structiedg0val 26321. (Contributed by AV, 23-Sep-2020.) (Revised by AV, 12-Nov-2021.) |
⊢ 𝑆 ∈ ℕ & ⊢ (Base‘ndx) < 𝑆 & ⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 2 ≤ (♯‘dom 𝐺)) | ||
Theorem | structvtxval 26320 | The set of vertices of an extensible structure with a base set and another slot. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.) |
⊢ 𝑆 ∈ ℕ & ⊢ (Base‘ndx) < 𝑆 & ⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘𝐺) = 𝑉) | ||
Theorem | structiedg0val 26321 | The set of indexed edges of an extensible structure with a base set and another slot not being the slot for edge functions is empty. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.) |
⊢ 𝑆 ∈ ℕ & ⊢ (Base‘ndx) < 𝑆 & ⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) → (iEdg‘𝐺) = ∅) | ||
Theorem | structgrssvtxlem 26322 | Lemma for structgrssvtx 26323 and structgrssiedg 26324. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.) |
⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 𝐸 ∈ 𝑍) & ⊢ (𝜑 → {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⊆ 𝐺) ⇒ ⊢ (𝜑 → 2 ≤ (♯‘dom 𝐺)) | ||
Theorem | structgrssvtx 26323 | The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.) |
⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 𝐸 ∈ 𝑍) & ⊢ (𝜑 → {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⊆ 𝐺) ⇒ ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) | ||
Theorem | structgrssiedg 26324 | The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.) |
⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 𝐸 ∈ 𝑍) & ⊢ (𝜑 → {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⊆ 𝐺) ⇒ ⊢ (𝜑 → (iEdg‘𝐺) = 𝐸) | ||
Theorem | struct2grstr 26325 | A graph represented as an extensible structure with vertices as base set and indexed edges is actually an extensible structure. (Contributed by AV, 23-Nov-2020.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⇒ ⊢ 𝐺 Struct 〈(Base‘ndx), (.ef‘ndx)〉 | ||
Theorem | struct2grvtx 26326 | The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 23-Sep-2020.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘𝐺) = 𝑉) | ||
Theorem | struct2griedg 26327 | The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘𝐺) = 𝐸) | ||
Theorem | graop 26328 | Any representation of a graph 𝐺 (especially as extensible structure 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉}) is convertible in a representation of the graph as ordered pair. (Contributed by AV, 7-Oct-2020.) |
⊢ 𝐻 = 〈(Vtx‘𝐺), (iEdg‘𝐺)〉 ⇒ ⊢ ((Vtx‘𝐺) = (Vtx‘𝐻) ∧ (iEdg‘𝐺) = (iEdg‘𝐻)) | ||
Theorem | grastruct 26329 | Any representation of a graph 𝐺 (especially as ordered pair 𝐺 = 〈𝑉, 𝐸〉) is convertible in a representation of the graph as extensible structure. (Contributed by AV, 8-Oct-2020.) |
⊢ 𝐻 = {〈(Base‘ndx), (Vtx‘𝐺)〉, 〈(.ef‘ndx), (iEdg‘𝐺)〉} ⇒ ⊢ ((Vtx‘𝐺) = (Vtx‘𝐻) ∧ (iEdg‘𝐺) = (iEdg‘𝐻)) | ||
Theorem | gropd 26330* | If any representation of a graph with vertices 𝑉 and edges 𝐸 has a certain property 𝜓, then the ordered pair 〈𝑉, 𝐸〉 of the set of vertices and the set of edges (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) has this property. (Contributed by AV, 11-Oct-2020.) |
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝜓)) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) ⇒ ⊢ (𝜑 → [〈𝑉, 𝐸〉 / 𝑔]𝜓) | ||
Theorem | grstructd 26331* | If any representation of a graph with vertices 𝑉 and edges 𝐸 has a certain property 𝜓, then any structure with base set 𝑉 and value 𝐸 in the slot for edge functions (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) has this property. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 9-Jun-2021.) |
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝜓)) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) & ⊢ (𝜑 → Fun (𝑆 ∖ {∅})) & ⊢ (𝜑 → 2 ≤ (♯‘dom 𝑆)) & ⊢ (𝜑 → (Base‘𝑆) = 𝑉) & ⊢ (𝜑 → (.ef‘𝑆) = 𝐸) ⇒ ⊢ (𝜑 → [𝑆 / 𝑔]𝜓) | ||
Theorem | gropeld 26332* | If any representation of a graph with vertices 𝑉 and edges 𝐸 is an element of an arbitrary class 𝐶, then the ordered pair 〈𝑉, 𝐸〉 of the set of vertices and the set of edges (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) is an element of this class 𝐶. (Contributed by AV, 11-Oct-2020.) |
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝑔 ∈ 𝐶)) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) ⇒ ⊢ (𝜑 → 〈𝑉, 𝐸〉 ∈ 𝐶) | ||
Theorem | grstructeld 26333* | If any representation of a graph with vertices 𝑉 and edges 𝐸 is an element of an arbitrary class 𝐶, then any structure with base set 𝑉 and value 𝐸 in the slot for edge functions (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) is an element of this class 𝐶. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 9-Jun-2021.) |
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝑔 ∈ 𝐶)) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) & ⊢ (𝜑 → Fun (𝑆 ∖ {∅})) & ⊢ (𝜑 → 2 ≤ (♯‘dom 𝑆)) & ⊢ (𝜑 → (Base‘𝑆) = 𝑉) & ⊢ (𝜑 → (.ef‘𝑆) = 𝐸) ⇒ ⊢ (𝜑 → 𝑆 ∈ 𝐶) | ||
Theorem | setsvtx 26334 | The vertices of a structure with a base set and an inserted resp. replaced slot for the edge function. (Contributed by AV, 18-Jan-2020.) (Revised by AV, 16-Nov-2021.) |
⊢ 𝐼 = (.ef‘ndx) & ⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝐺) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) ⇒ ⊢ (𝜑 → (Vtx‘(𝐺 sSet 〈𝐼, 𝐸〉)) = (Base‘𝐺)) | ||
Theorem | setsiedg 26335 | The (indexed) edges of a structure with a base set and an inserted resp. replaced slot for the edge function. (Contributed by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.) |
⊢ 𝐼 = (.ef‘ndx) & ⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝐺) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) ⇒ ⊢ (𝜑 → (iEdg‘(𝐺 sSet 〈𝐼, 𝐸〉)) = 𝐸) | ||
Theorem | snstrvtxval 26336 | The set of vertices of a graph without edges represented as an extensible structure with vertices as base set and no indexed edges. See vtxvalsnop 26340 for the (degenerate) case where 𝑉 = (Base‘ndx). (Contributed by AV, 23-Sep-2020.) |
⊢ 𝑉 ∈ V & ⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉} ⇒ ⊢ (𝑉 ≠ (Base‘ndx) → (Vtx‘𝐺) = 𝑉) | ||
Theorem | snstriedgval 26337 | The set of indexed edges of a graph without edges represented as an extensible structure with vertices as base set and no indexed edges. See iedgvalsnop 26341 for the (degenerate) case where 𝑉 = (Base‘ndx). (Contributed by AV, 24-Sep-2020.) |
⊢ 𝑉 ∈ V & ⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉} ⇒ ⊢ (𝑉 ≠ (Base‘ndx) → (iEdg‘𝐺) = ∅) | ||
Theorem | vtxval0 26338 | Degenerated case 1 for vertices: The set of vertices of the empty set is the empty set. (Contributed by AV, 24-Sep-2020.) |
⊢ (Vtx‘∅) = ∅ | ||
Theorem | iedgval0 26339 | Degenerated case 1 for edges: The set of indexed edges of the empty set is the empty set. (Contributed by AV, 24-Sep-2020.) |
⊢ (iEdg‘∅) = ∅ | ||
Theorem | vtxvalsnop 26340 | Degenerated case 2 for vertices: The set of vertices of a singleton containing an ordered pair with equal components is the singleton containing the component. (Contributed by AV, 24-Sep-2020.) (Proof shortened by AV, 15-Jul-2022.) (Avoid depending on this detail.) |
⊢ 𝐵 ∈ V & ⊢ 𝐺 = {〈𝐵, 𝐵〉} ⇒ ⊢ (Vtx‘𝐺) = {𝐵} | ||
Theorem | iedgvalsnop 26341 | Degenerated case 2 for edges: The set of indexed edges of a singleton containing an ordered pair with equal components is the singleton containing the component. (Contributed by AV, 24-Sep-2020.) (Proof shortened by AV, 15-Jul-2022.) (Avoid depending on this detail.) |
⊢ 𝐵 ∈ V & ⊢ 𝐺 = {〈𝐵, 𝐵〉} ⇒ ⊢ (iEdg‘𝐺) = {𝐵} | ||
Theorem | vtxval3sn 26342 | Degenerated case 3 for vertices: The set of vertices of a singleton containing a singleton containing a singleton is the innermost singleton. (Contributed by AV, 24-Sep-2020.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (Vtx‘{{{𝐴}}}) = {𝐴} | ||
Theorem | iedgval3sn 26343 | Degenerated case 3 for edges: The set of indexed edges of a singleton containing a singleton containing a singleton is the innermost singleton. (Contributed by AV, 24-Sep-2020.) (Avoid depending on this detail.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (iEdg‘{{{𝐴}}}) = {𝐴} | ||
Theorem | vtxvalprc 26344 | Degenerated case 4 for vertices: The set of vertices of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.) |
⊢ (𝐶 ∉ V → (Vtx‘𝐶) = ∅) | ||
Theorem | iedgvalprc 26345 | Degenerated case 4 for edges: The set of indexed edges of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.) |
⊢ (𝐶 ∉ V → (iEdg‘𝐶) = ∅) | ||
Syntax | cedg 26346 | Extend class notation with the set of edges (of an undirected simple (hyper-/pseudo-)graph). |
class Edg | ||
Definition | df-edg 26347 | Define the class of edges of a graph, see also definition "E = E(G)" in section I.1 of [Bollobas] p. 1. This definition is very general: It defines edges of a class as the range of its edge function (which does not even need to be a function). Therefore, this definition could also be used for hypergraphs, pseudographs and multigraphs. In these cases, however, the (possibly more than one) edges connecting the same vertices could not be distinguished anymore. In some cases, this is no problem, so theorems with Edg are meaningful nevertheless (e.g., edguhgr 26428). Usually, however, this definition is used only for undirected simple (hyper-/pseudo-)graphs (with or without loops). (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) |
⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔)) | ||
Theorem | edgval 26348 | The edges of a graph. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) (Revised by AV, 8-Dec-2021.) |
⊢ (Edg‘𝐺) = ran (iEdg‘𝐺) | ||
Theorem | iedgedg 26349 | An indexed edge is an edge. (Contributed by AV, 19-Dec-2021.) |
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((Fun 𝐸 ∧ 𝐼 ∈ dom 𝐸) → (𝐸‘𝐼) ∈ (Edg‘𝐺)) | ||
Theorem | edgopval 26350 | The edges of a graph represented as ordered pair. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (Edg‘〈𝑉, 𝐸〉) = ran 𝐸) | ||
Theorem | edgov 26351 | The edges of a graph represented as ordered pair, shown as operation value. Although a little less intuitive, this representation is often used because it is shorter than the representation as function value of a graph given as ordered pair, see edgopval 26350. The representation ran 𝐸 for the set of edges is even shorter, though. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 13-Oct-2020.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉Edg𝐸) = ran 𝐸) | ||
Theorem | edgstruct 26352 | The edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 13-Oct-2020.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (Edg‘𝐺) = ran 𝐸) | ||
Theorem | edgiedgb 26353* | A set is an edge iff it is an indexed edge. (Contributed by AV, 17-Oct-2020.) (Revised by AV, 8-Dec-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (Fun 𝐼 → (𝐸 ∈ (Edg‘𝐺) ↔ ∃𝑥 ∈ dom 𝐼 𝐸 = (𝐼‘𝑥))) | ||
Theorem | edg0iedg0 26354 | There is no edge in a graph iff its edge function is empty. (Contributed by AV, 15-Dec-2020.) (Revised by AV, 8-Dec-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (Fun 𝐼 → (𝐸 = ∅ ↔ 𝐼 = ∅)) | ||
For undirected graphs, we will have the following hierarchy/taxonomy: * Undirected Hypergraph: UHGraph * Undirected loop-free graphs: ULFGraph (not defined formally yet) * Undirected simple Hypergraph: USHGraph => USHGraph ⊆ UHGraph (ushgruhgr 26368) * Undirected Pseudograph: UPGraph => UPGraph ⊆ UHGraph (upgruhgr 26401) * Undirected loop-free hypergraph: ULFHGraph (not defined formally yet) => ULFHGraph ⊆ UHGraph and ULFHGraph ⊆ ULFGraph * Undirected loop-free simple hypergraph: ULFSHGraph (not defined formally yet) => ULFSHGraph ⊆ USHGraph and ULFSHGraph ⊆ ULFHGraph * Undirected simple Pseudograph: USPGraph => USPGraph ⊆ UPGraph (uspgrupgr 26476) and USPGraph ⊆ USHGraph (uspgrushgr 26475), see also uspgrupgrushgr 26477 * Undirected Muligraph: UMGraph => UMGraph ⊆ UPGraph (umgrupgr 26402) and UMGraph ⊆ ULFHGraph (umgrislfupgr 26422) * Undirected simple Graph: USGraph => USGraph ⊆ USPGraph (usgruspgr 26478) and USGraph ⊆ UMGraph (usgrumgr 26479) and USGraph ⊆ ULFSHGraph (usgrislfuspgr 26484) see also usgrumgruspgr 26480 | ||
Syntax | cuhgr 26355 | Extend class notation with undirected hypergraphs. |
class UHGraph | ||
Syntax | cushgr 26356 | Extend class notation with undirected simple hypergraphs. |
class USHGraph | ||
Definition | df-uhgr 26357* | Define the class of all undirected hypergraphs. An undirected hypergraph consists of a set 𝑣 (of "vertices") and a function 𝑒 (representing indexed "edges") into the power set of this set (the empty set excluded). (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 8-Oct-2020.) |
⊢ UHGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})} | ||
Definition | df-ushgr 26358* | Define the class of all undirected simple hypergraphs. An undirected simple hypergraph is a special (non-simple, multiple, multi-) hypergraph for which the edge function 𝑒 is an injective (one-to-one) function into subsets of the set of vertices 𝑣, representing the (one or more) vertices incident to the edge. This definition corresponds to the definition of hypergraphs in section I.1 of [Bollobas] p. 7 (except that the empty set seems to be allowed to be an "edge") or section 1.10 of [Diestel] p. 27, where "E is a subset of [...] the power set of V, that is the set of all subsets of V" resp. "the elements of E are nonempty subsets (of any cardinality) of V". (Contributed by AV, 19-Jan-2020.) (Revised by AV, 8-Oct-2020.) |
⊢ USHGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅})} | ||
Theorem | isuhgr 26359 | The predicate "is an undirected hypergraph." (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 9-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UHGraph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) | ||
Theorem | isushgr 26360 | The predicate "is an undirected simple hypergraph." (Contributed by AV, 19-Jan-2020.) (Revised by AV, 9-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ USHGraph ↔ 𝐸:dom 𝐸–1-1→(𝒫 𝑉 ∖ {∅}))) | ||
Theorem | uhgrf 26361 | The edge function of an undirected hypergraph is a function into the power set of the set of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 9-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UHGraph → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})) | ||
Theorem | ushgrf 26362 | The edge function of an undirected simple hypergraph is a one-to-one function into the power set of the set of vertices. (Contributed by AV, 9-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ USHGraph → 𝐸:dom 𝐸–1-1→(𝒫 𝑉 ∖ {∅})) | ||
Theorem | uhgrss 26363 | An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 18-Jan-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ dom 𝐸) → (𝐸‘𝐹) ⊆ 𝑉) | ||
Theorem | uhgreq12g 26364 | If two sets have the same vertices and the same edges, one set is a hypergraph iff the other set is a hypergraph. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 18-Jan-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝐹 = (iEdg‘𝐻) ⇒ ⊢ (((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝐺 ∈ UHGraph ↔ 𝐻 ∈ UHGraph)) | ||
Theorem | uhgrfun 26365 | The edge function of an undirected hypergraph is a function. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 15-Dec-2020.) |
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UHGraph → Fun 𝐸) | ||
Theorem | uhgrn0 26366 | An edge is a nonempty subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 15-Dec-2020.) |
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ≠ ∅) | ||
Theorem | lpvtx 26367 | The endpoints of a loop (which is an edge at index 𝐽) are two (identical) vertices 𝐴. (Contributed by AV, 1-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → 𝐴 ∈ (Vtx‘𝐺)) | ||
Theorem | ushgruhgr 26368 | An undirected simple hypergraph is an undirected hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 9-Oct-2020.) |
⊢ (𝐺 ∈ USHGraph → 𝐺 ∈ UHGraph) | ||
Theorem | isuhgrop 26369 | The property of being an undirected hypergraph represented as an ordered pair. The representation as an ordered pair is the usual representation of a graph, see section I.1 of [Bollobas] p. 1. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 9-Oct-2020.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (〈𝑉, 𝐸〉 ∈ UHGraph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) | ||
Theorem | uhgr0e 26370 | The empty graph, with vertices but no edges, is a hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 25-Nov-2020.) |
⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → (iEdg‘𝐺) = ∅) ⇒ ⊢ (𝜑 → 𝐺 ∈ UHGraph) | ||
Theorem | uhgr0vb 26371 | The null graph, with no vertices, is a hypergraph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 9-Oct-2020.) |
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → (𝐺 ∈ UHGraph ↔ (iEdg‘𝐺) = ∅)) | ||
Theorem | uhgr0 26372 | The null graph represented by an empty set is a hypergraph. (Contributed by AV, 9-Oct-2020.) |
⊢ ∅ ∈ UHGraph | ||
Theorem | uhgrun 26373 | The union 𝑈 of two (undirected) hypergraphs 𝐺 and 𝐻 with the same vertex set 𝑉 is a hypergraph with the vertex 𝑉 and the union (𝐸 ∪ 𝐹) of the (indexed) edges. (Contributed by AV, 11-Oct-2020.) (Revised by AV, 24-Oct-2021.) |
⊢ (𝜑 → 𝐺 ∈ UHGraph) & ⊢ (𝜑 → 𝐻 ∈ UHGraph) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) & ⊢ (𝜑 → 𝑈 ∈ 𝑊) & ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑈) = (𝐸 ∪ 𝐹)) ⇒ ⊢ (𝜑 → 𝑈 ∈ UHGraph) | ||
Theorem | uhgrunop 26374 | The union of two (undirected) hypergraphs (with the same vertex set) represented as ordered pair: If 〈𝑉, 𝐸〉 and 〈𝑉, 𝐹〉 are hypergraphs, then 〈𝑉, 𝐸 ∪ 𝐹〉 is a hypergraph (the vertex set stays the same, but the edges from both graphs are kept, possibly resulting in two edges between two vertices). (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 11-Oct-2020.) (Revised by AV, 24-Oct-2021.) |
⊢ (𝜑 → 𝐺 ∈ UHGraph) & ⊢ (𝜑 → 𝐻 ∈ UHGraph) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) ⇒ ⊢ (𝜑 → 〈𝑉, (𝐸 ∪ 𝐹)〉 ∈ UHGraph) | ||
Theorem | ushgrun 26375 | The union 𝑈 of two (undirected) simple hypergraphs 𝐺 and 𝐻 with the same vertex set 𝑉 is a (not necessarily simple) hypergraph with the vertex 𝑉 and the union (𝐸 ∪ 𝐹) of the (indexed) edges. (Contributed by AV, 29-Nov-2020.) (Revised by AV, 24-Oct-2021.) |
⊢ (𝜑 → 𝐺 ∈ USHGraph) & ⊢ (𝜑 → 𝐻 ∈ USHGraph) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) & ⊢ (𝜑 → 𝑈 ∈ 𝑊) & ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑈) = (𝐸 ∪ 𝐹)) ⇒ ⊢ (𝜑 → 𝑈 ∈ UHGraph) | ||
Theorem | ushgrunop 26376 | The union of two (undirected) simple hypergraphs (with the same vertex set) represented as ordered pair: If 〈𝑉, 𝐸〉 and 〈𝑉, 𝐹〉 are simple hypergraphs, then 〈𝑉, 𝐸 ∪ 𝐹〉 is a (not necessarily simple) hypergraph - the vertex set stays the same, but the edges from both graphs are kept, possibly resulting in two edges between two vertices. (Contributed by AV, 29-Nov-2020.) (Revised by AV, 24-Oct-2021.) |
⊢ (𝜑 → 𝐺 ∈ USHGraph) & ⊢ (𝜑 → 𝐻 ∈ USHGraph) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) ⇒ ⊢ (𝜑 → 〈𝑉, (𝐸 ∪ 𝐹)〉 ∈ UHGraph) | ||
Theorem | uhgrstrrepe 26377 | Replacing (or adding) the edges (between elements of the base set) of an extensible structure results in a hypergraph. Instead of requiring (𝜑 → 𝐺 Struct 𝑋), it would be sufficient to require (𝜑 → Fun (𝐺 ∖ {∅})) and (𝜑 → 𝐺 ∈ V). (Contributed by AV, 18-Jan-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.) |
⊢ 𝑉 = (Base‘𝐺) & ⊢ 𝐼 = (.ef‘ndx) & ⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝐺) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) & ⊢ (𝜑 → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})) ⇒ ⊢ (𝜑 → (𝐺 sSet 〈𝐼, 𝐸〉) ∈ UHGraph) | ||
Theorem | incistruhgr 26378* | An incidence structure 〈𝑃, 𝐿, 𝐼〉 "where 𝑃 is a set whose elements are called points, 𝐿 is a distinct set whose elements are called lines and 𝐼 ⊆ (𝑃 × 𝐿) is the incidence relation" (see Wikipedia "Incidence structure" (24-Oct-2020), https://en.wikipedia.org/wiki/Incidence_structure) implies an undirected hypergraph, if the incidence relation is right-total (to exclude empty edges). The points become the vertices, and the edge function is derived from the incidence relation by mapping each line ("edge") to the set of vertices incident to the line/edge. With 𝑃 = (Base‘𝑆) and by defining two new slots for lines and incidence relations (analogous to LineG and Itv) and enhancing the definition of iEdg accordingly, it would even be possible to express that a corresponding incidence structure is an undirected hypergraph. By choosing the incident relation appropriately, other kinds of undirected graphs (pseudographs, multigraphs, simple graphs, etc.) could be defined. (Contributed by AV, 24-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿) → ((𝑉 = 𝑃 ∧ 𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑃 ∣ 𝑣𝐼𝑒})) → 𝐺 ∈ UHGraph)) | ||
Syntax | cupgr 26379 | Extend class notation with undirected pseudographs. |
class UPGraph | ||
Syntax | cumgr 26380 | Extend class notation with undirected multigraphs. |
class UMGraph | ||
Definition | df-upgr 26381* | Define the class of all undirected pseudographs. An (undirected) pseudograph consists of a set 𝑣 (of "vertices") and a function 𝑒 (representing indexed "edges") into subsets of 𝑣 of cardinality one or two, representing the two vertices incident to the edge, or the one vertex if the edge is a loop. This is according to Chartrand, Gary and Zhang, Ping (2012): "A First Course in Graph Theory.", Dover, ISBN 978-0-486-48368-9, section 1.4, p. 26: "In a pseudograph, not only are parallel edges permitted but an edge is also permitted to join a vertex to itself. Such an edge is called a loop." (in contrast to a multigraph, see df-umgr 26382). (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 24-Nov-2020.) |
⊢ UPGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}} | ||
Definition | df-umgr 26382* | Define the class of all undirected multigraphs. An (undirected) multigraph consists of a set 𝑣 (of "vertices") and a function 𝑒 (representing indexed "edges") into subsets of 𝑣 of cardinality two, representing the two vertices incident to the edge. In contrast to a pseudograph, a multigraph has no loop. This is according to Chartrand, Gary and Zhang, Ping (2012): "A First Course in Graph Theory.", Dover, ISBN 978-0-486-48368-9, section 1.4, p. 26: "A multigraph M consists of a finite nonempty set V of vertices and a set E of edges, where every two vertices of M are joined by a finite number of edges (possibly zero). If two or more edges join the same pair of (distinct) vertices, then these edges are called parallel edges." To provide uniform definitions for all kinds of graphs, 𝑥 ∈ (𝒫 𝑣 ∖ {∅}) is used as restriction of the class abstraction, although 𝑥 ∈ 𝒫 𝑣 would be sufficient (see prprrab 13545 and isumgrs 26395). (Contributed by AV, 24-Nov-2020.) |
⊢ UMGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) = 2}} | ||
Theorem | isupgr 26383* | The property of being an undirected pseudograph. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UPGraph ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})) | ||
Theorem | wrdupgr 26384* | The property of being an undirected pseudograph, expressing the edges as "words". (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ Word 𝑋) → (𝐺 ∈ UPGraph ↔ 𝐸 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})) | ||
Theorem | upgrf 26385* | The edge function of an undirected pseudograph is a function into unordered pairs of vertices. Version of upgrfn 26386 without explicitly specified domain of the edge function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UPGraph → 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}) | ||
Theorem | upgrfn 26386* | The edge function of an undirected pseudograph is a function into unordered pairs of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴) → 𝐸:𝐴⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}) | ||
Theorem | upgrss 26387 | An edge is a subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 29-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ dom 𝐸) → (𝐸‘𝐹) ⊆ 𝑉) | ||
Theorem | upgrn0 26388 | An edge is a nonempty subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ≠ ∅) | ||
Theorem | upgrle 26389 | An edge of an undirected pseudograph has at most two ends. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (♯‘(𝐸‘𝐹)) ≤ 2) | ||
Theorem | upgrfi 26390 | An edge is a finite subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ∈ Fin) | ||
Theorem | upgrex 26391* | An edge is an unordered pair of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) | ||
Theorem | upgrbi 26392* | Show that an unordered pair is a valid edge in a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 28-Feb-2021.) |
⊢ 𝑋 ∈ 𝑉 & ⊢ 𝑌 ∈ 𝑉 ⇒ ⊢ {𝑋, 𝑌} ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} | ||
Theorem | upgrop 26393 | A pseudograph represented by an ordered pair. (Contributed by AV, 12-Dec-2021.) |
⊢ (𝐺 ∈ UPGraph → 〈(Vtx‘𝐺), (iEdg‘𝐺)〉 ∈ UPGraph) | ||
Theorem | isumgr 26394* | The property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UMGraph ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) = 2})) | ||
Theorem | isumgrs 26395* | The simplified property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UMGraph ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})) | ||
Theorem | wrdumgr 26396* | The property of being an undirected multigraph, expressing the edges as "words". (Contributed by AV, 24-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ Word 𝑋) → (𝐺 ∈ UMGraph ↔ 𝐸 ∈ Word {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})) | ||
Theorem | umgrf 26397* | The edge function of an undirected multigraph is a function into unordered pairs of vertices. Version of umgrfn 26398 without explicitly specified domain of the edge function. (Contributed by AV, 24-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UMGraph → 𝐸:dom 𝐸⟶{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) | ||
Theorem | umgrfn 26398* | The edge function of an undirected multigraph is a function into unordered pairs of vertices. (Contributed by AV, 24-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝐸 Fn 𝐴) → 𝐸:𝐴⟶{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) | ||
Theorem | umgredg2 26399 | An edge of a multigraph has exactly two ends. (Contributed by AV, 24-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸) → (♯‘(𝐸‘𝑋)) = 2) | ||
Theorem | umgrbi 26400* | Show that an unordered pair is a valid edge in a multigraph. (Contributed by AV, 9-Mar-2021.) |
⊢ 𝑋 ∈ 𝑉 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑋 ≠ 𝑌 ⇒ ⊢ {𝑋, 𝑌} ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |