![]() |
Metamath
Proof Explorer Theorem List (p. 265 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | edgstruct 26401 | 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 26402* | 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 26403 | 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 26417) * Undirected Pseudograph: UPGraph => UPGraph ⊆ UHGraph (upgruhgr 26450) * 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 26525) and USPGraph ⊆ USHGraph (uspgrushgr 26524), see also uspgrupgrushgr 26526 * Undirected Muligraph: UMGraph => UMGraph ⊆ UPGraph (umgrupgr 26451) and UMGraph ⊆ ULFHGraph (umgrislfupgr 26471) * Undirected simple Graph: USGraph => USGraph ⊆ USPGraph (usgruspgr 26527) and USGraph ⊆ UMGraph (usgrumgr 26528) and USGraph ⊆ ULFSHGraph (usgrislfuspgr 26533) see also usgrumgruspgr 26529 | ||
Syntax | cuhgr 26404 | Extend class notation with undirected hypergraphs. |
class UHGraph | ||
Syntax | cushgr 26405 | Extend class notation with undirected simple hypergraphs. |
class USHGraph | ||
Definition | df-uhgr 26406* | 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 26407* | 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 26408 | 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 26409 | 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 26410 | 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 26411 | 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 26412 | 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 26413 | 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 26414 | 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 26415 | 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 26416 | 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 26417 | An undirected simple hypergraph is an undirected hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 9-Oct-2020.) |
⊢ (𝐺 ∈ USHGraph → 𝐺 ∈ UHGraph) | ||
Theorem | isuhgrop 26418 | 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 26419 | 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 26420 | 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 26421 | The null graph represented by an empty set is a hypergraph. (Contributed by AV, 9-Oct-2020.) |
⊢ ∅ ∈ UHGraph | ||
Theorem | uhgrun 26422 | 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 26423 | 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 26424 | 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 26425 | 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 26426 | 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 26427* | 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 26428 | Extend class notation with undirected pseudographs. |
class UPGraph | ||
Syntax | cumgr 26429 | Extend class notation with undirected multigraphs. |
class UMGraph | ||
Definition | df-upgr 26430* | 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 26431). (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 24-Nov-2020.) |
⊢ UPGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}} | ||
Definition | df-umgr 26431* | 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 13569 and isumgrs 26444). (Contributed by AV, 24-Nov-2020.) |
⊢ UMGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) = 2}} | ||
Theorem | isupgr 26432* | 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 26433* | 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 26434* | The edge function of an undirected pseudograph is a function into unordered pairs of vertices. Version of upgrfn 26435 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 26435* | 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 26436 | 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 26437 | 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 26438 | 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 26439 | 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 26440* | 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 26441* | 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 26442 | A pseudograph represented by an ordered pair. (Contributed by AV, 12-Dec-2021.) |
⊢ (𝐺 ∈ UPGraph → 〈(Vtx‘𝐺), (iEdg‘𝐺)〉 ∈ UPGraph) | ||
Theorem | isumgr 26443* | The property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UMGraph ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) = 2})) | ||
Theorem | isumgrs 26444* | The simplified property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UMGraph ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})) | ||
Theorem | wrdumgr 26445* | 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 26446* | The edge function of an undirected multigraph is a function into unordered pairs of vertices. Version of umgrfn 26447 without explicitly specified domain of the edge function. (Contributed by AV, 24-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UMGraph → 𝐸:dom 𝐸⟶{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) | ||
Theorem | umgrfn 26447* | 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 26448 | An edge of a multigraph has exactly two ends. (Contributed by AV, 24-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸) → (♯‘(𝐸‘𝑋)) = 2) | ||
Theorem | umgrbi 26449* | Show that an unordered pair is a valid edge in a multigraph. (Contributed by AV, 9-Mar-2021.) |
⊢ 𝑋 ∈ 𝑉 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑋 ≠ 𝑌 ⇒ ⊢ {𝑋, 𝑌} ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} | ||
Theorem | upgruhgr 26450 | An undirected pseudograph is an undirected hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 10-Oct-2020.) |
⊢ (𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph) | ||
Theorem | umgrupgr 26451 | An undirected multigraph is an undirected pseudograph. (Contributed by AV, 25-Nov-2020.) |
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph) | ||
Theorem | umgruhgr 26452 | An undirected multigraph is an undirected hypergraph. (Contributed by AV, 26-Nov-2020.) |
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph) | ||
Theorem | upgrle2 26453 | An edge of an undirected pseudograph has at most two ends. (Contributed by AV, 6-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑋 ∈ dom 𝐼) → (♯‘(𝐼‘𝑋)) ≤ 2) | ||
Theorem | umgrnloopv 26454 | In a multigraph, there is no loop, i.e. no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Revised by AV, 11-Dec-2020.) |
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑀 ∈ 𝑊) → ((𝐸‘𝑋) = {𝑀, 𝑁} → 𝑀 ≠ 𝑁)) | ||
Theorem | umgredgprv 26455 | In a multigraph, an edge is an unordered pair of vertices. This theorem would not hold for arbitrary hyper-/pseudographs since either 𝑀 or 𝑁 could be proper classes ((𝐸‘𝑋) would be a loop in this case), which are no vertices of course. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 11-Dec-2020.) |
⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸) → ((𝐸‘𝑋) = {𝑀, 𝑁} → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))) | ||
Theorem | umgrnloop 26456* | In a multigraph, there is no loop, i.e. no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 19-Aug-2017.) (Revised by AV, 11-Dec-2020.) |
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UMGraph → (∃𝑥 ∈ dom 𝐸(𝐸‘𝑥) = {𝑀, 𝑁} → 𝑀 ≠ 𝑁)) | ||
Theorem | umgrnloop0 26457* | A multigraph has no loops. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 11-Dec-2020.) |
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UMGraph → {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅) | ||
Theorem | umgr0e 26458 | The empty graph, with vertices but no edges, is a multigraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 25-Nov-2020.) |
⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → (iEdg‘𝐺) = ∅) ⇒ ⊢ (𝜑 → 𝐺 ∈ UMGraph) | ||
Theorem | upgr0e 26459 | The empty graph, with vertices but no edges, is a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 11-Oct-2020.) (Proof shortened by AV, 25-Nov-2020.) |
⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → (iEdg‘𝐺) = ∅) ⇒ ⊢ (𝜑 → 𝐺 ∈ UPGraph) | ||
Theorem | upgr1elem 26460* | Lemma for upgr1e 26461 and uspgr1e 26591. (Contributed by AV, 16-Oct-2020.) |
⊢ (𝜑 → {𝐵, 𝐶} ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → {{𝐵, 𝐶}} ⊆ {𝑥 ∈ (𝑆 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}) | ||
Theorem | upgr1e 26461 | A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1e 26591. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 16-Oct-2020.) (Revised by AV, 21-Mar-2021.) (Proof shortened by AV, 17-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) ⇒ ⊢ (𝜑 → 𝐺 ∈ UPGraph) | ||
Theorem | upgr0eop 26462 | The empty graph, with vertices but no edges, is a pseudograph. The empty graph is actually a simple graph, see usgr0eop 26593, and therefore also a multigraph (𝐺 ∈ UMGraph). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 11-Oct-2020.) |
⊢ (𝑉 ∈ 𝑊 → 〈𝑉, ∅〉 ∈ UPGraph) | ||
Theorem | upgr1eop 26463 | A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1eop 26594. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 〈𝑉, {〈𝐴, {𝐵, 𝐶}〉}〉 ∈ UPGraph) | ||
Theorem | upgr0eopALT 26464 | Alternate proof of upgr0eop 26462, using the general theorem gropeld 26381 to transform a theorem for an arbitrary representation of a graph into a theorem for a graph represented as ordered pair. This general approach causes some overhead, which makes the proof longer than necessary (see proof of upgr0eop 26462). (Contributed by AV, 11-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑉 ∈ 𝑊 → 〈𝑉, ∅〉 ∈ UPGraph) | ||
Theorem | upgr1eopALT 26465 | Alternate proof of upgr1eop 26463, using the general theorem gropeld 26381 to transform a theorem for an arbitrary representation of a graph into a theorem for a graph represented as ordered pair. This general approach causes some overhead, which makes the proof longer than necessary (see proof of upgr1eop 26463). (Contributed by AV, 11-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 〈𝑉, {〈𝐴, {𝐵, 𝐶}〉}〉 ∈ UPGraph) | ||
Theorem | upgrun 26466 | The union 𝑈 of two pseudographs 𝐺 and 𝐻 with the same vertex set 𝑉 is a pseudograph with the vertex 𝑉 and the union (𝐸 ∪ 𝐹) of the (indexed) edges. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 24-Oct-2021.) |
⊢ (𝜑 → 𝐺 ∈ UPGraph) & ⊢ (𝜑 → 𝐻 ∈ UPGraph) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) & ⊢ (𝜑 → 𝑈 ∈ 𝑊) & ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑈) = (𝐸 ∪ 𝐹)) ⇒ ⊢ (𝜑 → 𝑈 ∈ UPGraph) | ||
Theorem | upgrunop 26467 | The union of two pseudographs (with the same vertex set): If 〈𝑉, 𝐸〉 and 〈𝑉, 𝐹〉 are pseudographs, then 〈𝑉, 𝐸 ∪ 𝐹〉 is a pseudograph (the vertex set stays the same, but the edges from both graphs are kept). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 12-Oct-2020.) (Revised by AV, 24-Oct-2021.) |
⊢ (𝜑 → 𝐺 ∈ UPGraph) & ⊢ (𝜑 → 𝐻 ∈ UPGraph) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) ⇒ ⊢ (𝜑 → 〈𝑉, (𝐸 ∪ 𝐹)〉 ∈ UPGraph) | ||
Theorem | umgrun 26468 | The union 𝑈 of two multigraphs 𝐺 and 𝐻 with the same vertex set 𝑉 is a multigraph with the vertex 𝑉 and the union (𝐸 ∪ 𝐹) of the (indexed) edges. (Contributed by AV, 25-Nov-2020.) |
⊢ (𝜑 → 𝐺 ∈ UMGraph) & ⊢ (𝜑 → 𝐻 ∈ UMGraph) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) & ⊢ (𝜑 → 𝑈 ∈ 𝑊) & ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑈) = (𝐸 ∪ 𝐹)) ⇒ ⊢ (𝜑 → 𝑈 ∈ UMGraph) | ||
Theorem | umgrunop 26469 | The union of two multigraphs (with the same vertex set): If 〈𝑉, 𝐸〉 and 〈𝑉, 𝐹〉 are multigraphs, then 〈𝑉, 𝐸 ∪ 𝐹〉 is a multigraph (the vertex set stays the same, but the edges from both graphs are kept). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 25-Nov-2020.) |
⊢ (𝜑 → 𝐺 ∈ UMGraph) & ⊢ (𝜑 → 𝐻 ∈ UMGraph) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) ⇒ ⊢ (𝜑 → 〈𝑉, (𝐸 ∪ 𝐹)〉 ∈ UMGraph) | ||
For a hypergraph, the property to be "loop-free" is expressed by 𝐼:dom 𝐼⟶𝐸 with 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} and 𝐼 = (iEdg‘𝐺). 𝐸 is the set of edges which connect at least two vertices. | ||
Theorem | umgrislfupgrlem 26470 | Lemma for umgrislfupgr 26471 and usgrislfuspgr 26533. (Contributed by AV, 27-Jan-2021.) |
⊢ ({𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2} ∩ {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) = {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) = 2} | ||
Theorem | umgrislfupgr 26471* | A multigraph is a loop-free pseudograph. (Contributed by AV, 27-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UMGraph ↔ (𝐺 ∈ UPGraph ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})) | ||
Theorem | lfgredgge2 26472* | An edge of a loop-free graph has at least two ends. (Contributed by AV, 23-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 & ⊢ 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ⇒ ⊢ ((𝐼:𝐴⟶𝐸 ∧ 𝑋 ∈ 𝐴) → 2 ≤ (♯‘(𝐼‘𝑋))) | ||
Theorem | lfgrnloop 26473* | A loop-free graph has no loops. (Contributed by AV, 23-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 & ⊢ 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ⇒ ⊢ (𝐼:𝐴⟶𝐸 → {𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑈}} = ∅) | ||
Theorem | uhgredgiedgb 26474* | In a hypergraph, a set is an edge iff it is an indexed edge. (Contributed by AV, 17-Oct-2020.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UHGraph → (𝐸 ∈ (Edg‘𝐺) ↔ ∃𝑥 ∈ dom 𝐼 𝐸 = (𝐼‘𝑥))) | ||
Theorem | uhgriedg0edg0 26475 | A hypergraph has no edges iff its edge function is empty. (Contributed by AV, 21-Oct-2020.) (Proof shortened by AV, 8-Dec-2021.) |
⊢ (𝐺 ∈ UHGraph → ((Edg‘𝐺) = ∅ ↔ (iEdg‘𝐺) = ∅)) | ||
Theorem | uhgredgn0 26476 | An edge of a hypergraph is a nonempty subset of vertices. (Contributed by AV, 28-Nov-2020.) |
⊢ ((𝐺 ∈ UHGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → 𝐸 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅})) | ||
Theorem | edguhgr 26477 | An edge of a hypergraph is a subset of vertices. (Contributed by AV, 26-Oct-2020.) (Proof shortened by AV, 28-Nov-2020.) |
⊢ ((𝐺 ∈ UHGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → 𝐸 ∈ 𝒫 (Vtx‘𝐺)) | ||
Theorem | uhgredgrnv 26478 | An edge of a hypergraph contains only vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 4-Jun-2021.) |
⊢ ((𝐺 ∈ UHGraph ∧ 𝐸 ∈ (Edg‘𝐺) ∧ 𝑁 ∈ 𝐸) → 𝑁 ∈ (Vtx‘𝐺)) | ||
Theorem | uhgredgss 26479 | The set of edges of a hypergraph is a subset of the power set of vertices without the empty set. (Contributed by AV, 29-Nov-2020.) |
⊢ (𝐺 ∈ UHGraph → (Edg‘𝐺) ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅})) | ||
Theorem | upgredgss 26480* | The set of edges of a pseudograph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 29-Nov-2020.) |
⊢ (𝐺 ∈ UPGraph → (Edg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}) | ||
Theorem | umgredgss 26481* | The set of edges of a multigraph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 25-Nov-2020.) |
⊢ (𝐺 ∈ UMGraph → (Edg‘𝐺) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2}) | ||
Theorem | edgupgr 26482 | Properties of an edge of a pseudograph. (Contributed by AV, 8-Nov-2020.) |
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝐸 ≠ ∅ ∧ (♯‘𝐸) ≤ 2)) | ||
Theorem | edgumgr 26483 | Properties of an edge of a multigraph. (Contributed by AV, 25-Nov-2020.) |
⊢ ((𝐺 ∈ UMGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ (♯‘𝐸) = 2)) | ||
Theorem | uhgrvtxedgiedgb 26484* | In a hypergraph, a vertex is incident with an edge iff it is contained in an element of the range of the edge function. (Contributed by AV, 24-Dec-2020.) (Revised by AV, 6-Jul-2022.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉) → (∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖) ↔ ∃𝑒 ∈ 𝐸 𝑈 ∈ 𝑒)) | ||
Theorem | uhgrvtxedgiedgbOLD 26485* | Obsolete version of uhgrvtxedgiedgb 26484 as of 6-Jul-2022. (Contributed by AV, 24-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉) → (∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖) ↔ ∃𝑒 ∈ 𝐸 𝑈 ∈ 𝑒)) | ||
Theorem | upgredg 26486* | For each edge in a pseudograph, there are two vertices which are connected by this edge. (Contributed by AV, 4-Nov-2020.) (Proof shortened by AV, 26-Nov-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝐶 = {𝑎, 𝑏}) | ||
Theorem | umgredg 26487* | For each edge in a multigraph, there are two distinct vertices which are connected by this edge. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 25-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝐶 ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝐶 = {𝑎, 𝑏})) | ||
Theorem | upgrpredgv 26488 | An edge of a pseudograph always connects two vertices if the edge contains two sets. The two vertices/sets need not necessarily be different (loops are allowed). (Contributed by AV, 18-Nov-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ (𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑊) ∧ {𝑀, 𝑁} ∈ 𝐸) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) | ||
Theorem | umgrpredgv 26489 | An edge of a multigraph always connects two vertices. Analogue of umgredgprv 26455. This theorem does not hold for arbitrary pseudographs: if either 𝑀 or 𝑁 is a proper class, then {𝑀, 𝑁} ∈ 𝐸 could still hold ({𝑀, 𝑁} would be either {𝑀} or {𝑁}, see prprc1 4532 or prprc2 4533, i.e. a loop), but 𝑀 ∈ 𝑉 or 𝑁 ∈ 𝑉 would not be true. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ {𝑀, 𝑁} ∈ 𝐸) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) | ||
Theorem | upgredg2vtx 26490* | For a vertex incident to an edge there is another vertex incident to the edge in a pseudograph. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 5-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ 𝐴 ∈ 𝐶) → ∃𝑏 ∈ 𝑉 𝐶 = {𝐴, 𝑏}) | ||
Theorem | upgredgpr 26491 | If a proper pair (of vertices) is a subset of an edge in a pseudograph, the pair is the edge. (Contributed by AV, 30-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ {𝐴, 𝐵} ⊆ 𝐶) ∧ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵)) → {𝐴, 𝐵} = 𝐶) | ||
Theorem | edglnl 26492* | The edges incident with a vertex 𝑁 are the edges joining 𝑁 with other vertices and the loops on 𝑁 in a pseudograph. (Contributed by AV, 18-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (∪ 𝑣 ∈ (𝑉 ∖ {𝑁}){𝑖 ∈ dom 𝐸 ∣ (𝑁 ∈ (𝐸‘𝑖) ∧ 𝑣 ∈ (𝐸‘𝑖))} ∪ {𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}}) = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}) | ||
Theorem | numedglnl 26493* | The number of edges incident with a vertex 𝑁 is the number of edges joining 𝑁 with other vertices and the number of loops on 𝑁 in a pseudograph of finite size. (Contributed by AV, 19-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin) ∧ 𝑁 ∈ 𝑉) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(♯‘{𝑖 ∈ dom 𝐸 ∣ (𝑁 ∈ (𝐸‘𝑖) ∧ 𝑣 ∈ (𝐸‘𝑖))}) + (♯‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}})) = (♯‘{𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)})) | ||
Theorem | umgredgne 26494 | An edge of a multigraph always connects two different vertices. Analogue of umgrnloopv 26454 resp. umgrnloop 26456. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ {𝑀, 𝑁} ∈ 𝐸) → 𝑀 ≠ 𝑁) | ||
Theorem | umgrnloop2 26495 | A multigraph has no loops. (Contributed by AV, 27-Oct-2020.) (Revised by AV, 30-Nov-2020.) |
⊢ (𝐺 ∈ UMGraph → {𝑁, 𝑁} ∉ (Edg‘𝐺)) | ||
Theorem | umgredgnlp 26496* | An edge of a multigraph is not a loop. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 8-Jun-2021.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝐶 ∈ 𝐸) → ¬ ∃𝑣 𝐶 = {𝑣}) | ||
In this section, "simple graph" will always stand for "undirected simple graph (without loops)" and "simple pseudograph" for "undirected simple pseudograph (which could have loops)". | ||
Syntax | cuspgr 26497 | Extend class notation with undirected simple pseudographs (which could have loops). |
class USPGraph | ||
Syntax | cusgr 26498 | Extend class notation with undirected simple graphs (without loops). |
class USGraph | ||
Definition | df-uspgr 26499* | Define the class of all undirected simple pseudographs (which could have loops). An undirected simple pseudograph is a special undirected pseudograph (see uspgrupgr 26525) or a special undirected simple hypergraph (see uspgrushgr 26524), consisting of a set 𝑣 (of "vertices") and an injective (one-to-one) 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. In contrast to a pseudograph, there is at most one edge between two vertices resp. at most one loop for a vertex. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.) |
⊢ USPGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}} | ||
Definition | df-usgr 26500* | Define the class of all undirected simple graphs (without loops). An undirected simple graph is a special undirected simple pseudograph (see usgruspgr 26527), consisting of a set 𝑣 (of "vertices") and an injective (one-to-one) function 𝑒 (representing (indexed) "edges") into subsets of 𝑣 of cardinality two, representing the two vertices incident to the edge. In contrast to an undirected simple pseudograph, an undirected simple graph has no loops (edges connecting a vertex with itself). (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 13-Oct-2020.) |
⊢ USGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) = 2}} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |