Home | Metamath
Proof Explorer Theorem List (p. 259 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgriedg0edg0 25801 | A hypergraph has no edges iff its edge function is empty. (Contributed by AV, 21-Oct-2020.) (Proof shortened by AV, 15-Dec-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ UHGraph → ((Edg‘𝐺) = ∅ ↔ (iEdg‘𝐺) = ∅)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgredgn0 25802 | An edge of a hypergraph is a nonempty subset of vertices. (Contributed by AV, 28-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐺 ∈ UHGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → 𝐸 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edguhgr 25803 | 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 25804 | 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 25805 | The set of edges of a hypergraph is a subset of the powerset of vertices without the empty set. (Contributed by AV, 29-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ UHGraph → (Edg‘𝐺) ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | upgredgss 25806* | 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 25807* | 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 25808 | Properties of an edge of a pseudograph. (Contributed by AV, 8-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝐸 ≠ ∅ ∧ (#‘𝐸) ≤ 2)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgumgr 25809 | Properties of an edge of a multigraph. (Contributed by AV, 25-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐺 ∈ UMGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ (#‘𝐸) = 2)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgrvtxedgiedgb 25810* | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉) → (∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖) ↔ ∃𝑒 ∈ 𝐸 𝑈 ∈ 𝑒)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | upgredg 25811* | For each edge in a pseudograph, there are two vertices which are connected by this edge. (Contributed by AV, 4-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝐶 = {𝑎, 𝑏}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | umgredg 25812* | 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 | umgrpredgav 25813 | An edge of a multigraph always connects two vertices. Analogue of umgredgprv 25773. 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 4243 or prprc2 4244, i.e. a loop), but 𝑀 ∈ 𝑉 or 𝑁 ∈ 𝑉 would not be true. (Contributed by AV, 27-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ {𝑀, 𝑁} ∈ 𝐸) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | upgredg2vtx 25814* | 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 25815 | 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 | umgredgne 25816 | An edge of a multigraph always connects two different vertices. Analog of umgrnloopv 25772 resp. umgrnloop 25774. (Contributed by AV, 27-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ {𝑀, 𝑁} ∈ 𝐸) → 𝑀 ≠ 𝑁) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | umgrnloop2 25817 | A multigraph has no loops. (Contributed by AV, 27-Oct-2020.) (Revised by AV, 30-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ UMGraph → {𝑁, 𝑁} ∉ (Edg‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | umgredgnlp 25818* | An edge of a multigraph is not a loop. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 8-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝐶 ∈ 𝐸) → ¬ ∃𝑣 𝐶 = {𝑣}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Terms and properties of graphs:
Special kinds of graphs:
For the terms "Path", "Walk", "Trail", "Circuit", "Cycle" see the remarks below and the definitions in Section I.1 in [Bollobas] p. 4-5. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cuhg 25819 | Extend class notation with undirected hypergraphs. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class UHGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cushg 25820 | Extend class notation with undirected simple hypergraphs. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class USHGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-uhgra 25821* | Define the class of all undirected hypergraphs. An undirected hypergraph is a pair of a set and a function into the powerset of this set (the empty set excluded). (Contributed by Alexander van der Vekens, 26-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ UHGrph = {〈𝑣, 𝑒〉 ∣ 𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-ushgra 25822* | Define the class of all undirected simple hypergraphs. An undirected simple hypergraph is a pair of a set and an injective (one-to-one) function into the powerset of this set (the empty set excluded). (Contributed by AV, 19-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ USHGrph = {〈𝑣, 𝑒〉 ∣ 𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅})} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | reluhgra 25823 | The class of all undirected hypergraphs is a relation. (Contributed by Alexander van der Vekens, 26-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Rel UHGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | relushgra 25824 | The class of all undirected simple hypergraphs is a relation. (Contributed by AV, 19-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Rel USHGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgrav 25825 | The classes of vertices and edges of an undirected hypergraph are sets. (Contributed by Alexander van der Vekens, 26-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 UHGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgraopelvv 25826 | An undirected hypergraph is a member in the universal class of ordered pairs. (Contributed by AV, 3-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ UHGrph → 𝐺 ∈ (V × V)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isuhgra 25827 | The property of being an undirected hypergraph. (Contributed by Alexander van der Vekens, 26-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉 UHGrph 𝐸 ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgraf 25828 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 UHGrph 𝐸 → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgrafun 25829 | The edge function of an undirected hypergraph is a function. (Contributed by Alexander van der Vekens, 26-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 UHGrph 𝐸 → Fun 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isushgra 25830 | The property of being an undirected simple hypergraph. (Contributed by AV, 3-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉 USHGrph 𝐸 ↔ 𝐸:dom 𝐸–1-1→(𝒫 𝑉 ∖ {∅}))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ushgraf 25831 | The edge function of an undirected simple hypergraph is a function into the power set of the set of vertices. (Contributed by AV, 19-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USHGrph 𝐸 → 𝐸:dom 𝐸–1-1→(𝒫 𝑉 ∖ {∅})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ushgrauhgra 25832 | An undirected simple hypergraph is an undirected hypergraph. (Contributed by AV, 19-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USHGrph 𝐸 → 𝑉 UHGrph 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgraop 25833 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (〈𝑉, 𝐸〉 ∈ UHGrph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgrac 25834 | The property of being an undirected hypergraph represented by a class. This representation is useful if the set of vertices and the edge function is/needs not to be known. (Contributed by AV, 1-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ UHGrph → (2nd ‘𝐺):dom (2nd ‘𝐺)⟶(𝒫 (1st ‘𝐺) ∖ {∅})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgrass 25835 | An edge is a subset of vertices, analogous to umgrass 25848. (Contributed by Alexander van der Vekens, 26-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 UHGrph 𝐸 ∧ 𝐹 ∈ dom 𝐸) → (𝐸‘𝐹) ⊆ 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgraeq12d 25836 | Equality of hypergraphs. (Contributed by Alexander van der Vekens, 26-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝑉 UHGrph 𝐸 ↔ 𝑊 UHGrph 𝐹)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgrares 25837 | A subgraph of a hypergraph (formed by removing some edges from the original graph) is a hypergraph, analogous to umgrares 25853. (Contributed by Alexander van der Vekens, 27-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 UHGrph 𝐸 → 𝑉 UHGrph (𝐸 ↾ 𝐴)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgra0 25838 | The empty graph, with vertices but no edges, is a hypergraph, analogous to umgra0 25854. (Contributed by Alexander van der Vekens, 27-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 ∈ 𝑊 → 𝑉 UHGrph ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgra0v 25839 | 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.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (∅ UHGrph 𝐸 ↔ 𝐸 = ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgraun 25840 | The union of two (undirected) hypergraphs (with the same vertex set): 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), analogous to umgraun 25857. (Contributed by Alexander van der Vekens, 27-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐸 Fn 𝐴) & ⊢ (𝜑 → 𝐹 Fn 𝐵) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝑉 UHGrph 𝐸) & ⊢ (𝜑 → 𝑉 UHGrph 𝐹) ⇒ ⊢ (𝜑 → 𝑉 UHGrph (𝐸 ∪ 𝐹)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cumg 25841 | Extend class notation with undirected multigraphs. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class UMGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-umgra 25842* | Define the class of all undirected multigraphs. A multigraph is a pair 〈𝑉, 𝐸〉 where 𝐸 is a function 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. (Contributed by Mario Carneiro, 11-Mar-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ UMGrph = {〈𝑣, 𝑒〉 ∣ 𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | relumgra 25843 | The class of all undirected multigraphs is a relation. (Contributed by Mario Carneiro, 11-Mar-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Rel UMGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isumgra 25844* | The property of being an undirected multigraph. (Contributed by Mario Carneiro, 11-Mar-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉 UMGrph 𝐸 ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdumgra 25845* | The property of being an undirected multigraph, expressing the edges as "words". (Contributed by Mario Carneiro, 11-Mar-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ Word 𝑋) → (𝑉 UMGrph 𝐸 ↔ 𝐸 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | umgraf2 25846* | The edge function of an undirected multigraph is a function into unordered pairs of vertices. Version of umgraf 25847 without explicitly specified domain of the edge function. (Contributed by Mario Carneiro, 12-Mar-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 UMGrph 𝐸 → 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | umgraf 25847* | The edge function of an undirected multigraph is a function into unordered pairs of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴) → 𝐸:𝐴⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | umgrass 25848 | An edge is a subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ⊆ 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | umgran0 25849 | An edge is a nonempty subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ≠ ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | umgrale 25850 | An edge has at most two ends. (Contributed by Mario Carneiro, 11-Mar-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (#‘(𝐸‘𝐹)) ≤ 2) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | umgrafi 25851 | An edge is a finite subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ∈ Fin) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | umgraex 25852* | An edge is an unordered pair of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | umgrares 25853 | A subgraph of a graph (formed by removing some edges from the original graph) is a graph. (Contributed by Mario Carneiro, 12-Mar-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 UMGrph 𝐸 → 𝑉 UMGrph (𝐸 ↾ 𝐴)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | umgra0 25854 | The empty graph, with vertices but no edges, is a graph. (Contributed by Mario Carneiro, 12-Mar-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 ∈ 𝑊 → 𝑉 UMGrph ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | umgra1 25855 | The graph with one edge. (Contributed by Mario Carneiro, 12-Mar-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝑉 UMGrph {〈𝐴, {𝐵, 𝐶}〉}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | umisuhgra 25856 | An undirected multigraph is an undirected hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 UMGrph 𝐸 → 𝑉 UHGrph 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | umgraun 25857 | The union of two (undirected) multigraphs (with the same vertex set): If 〈𝑉, 𝐸〉 and 〈𝑉, 𝐹〉 are graphs, then 〈𝑉, 𝐸 ∪ 𝐹〉 is a graph (the vertex set stays the same, but the edges from both graphs are kept). (Contributed by Mario Carneiro, 12-Mar-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐸 Fn 𝐴) & ⊢ (𝜑 → 𝐹 Fn 𝐵) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝑉 UMGrph 𝐸) & ⊢ (𝜑 → 𝑉 UMGrph 𝐹) ⇒ ⊢ (𝜑 → 𝑉 UMGrph (𝐸 ∪ 𝐹)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cuslg 25858 | Extend class notation with undirected (simple) graphs with loops. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class USLGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cusg 25859 | Extend class notation with undirected (simple) graphs (without loops). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class USGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cedg 25860 | Extend class notation with the set of edges (of an undirected simple graph). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class Edges | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-uslgra 25861* | Define the class of all undirected simple graphs with loops. An undirected simple graph with loops is a special undirected multigraph 〈𝑉, 𝐸〉 where 𝐸 is an injective (one-to-one) function 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 multigraph, there is at most one edge between two vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ USLGrph = {〈𝑣, 𝑒〉 ∣ 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-usgra 25862* | Define the class of all undirected simple graphs without loops. An undirected simple graph without loops is a special undirected simple graph 〈𝑉, 𝐸〉 where 𝐸 is an injective (one-to-one) function into subsets of 𝑉 of cardinality two, representing the two vertices incident to the edge. Such graphs are usually simply called "undirected graphs", so if only the term "undirected graph" is used, an undirected simple graph without loops is meant. Therefore, an undirected graph has no loops (edges a vertex to itself). (Contributed by Alexander van der Vekens, 10-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ USGrph = {〈𝑣, 𝑒〉 ∣ 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2}} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | reluslgra 25863 | The class of all undirected simple graph with loops is a relation. (Contributed by Alexander van der Vekens, 10-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Rel USLGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | relusgra 25864 | The class of all undirected simple graph without loops is a relation. (Contributed by Alexander van der Vekens, 10-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Rel USGrph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-edg 25865 | 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 for any ordered pairs as the range of its second component (which even needs not to be a function). Therefore, this definition could also be used for hypergraphs and multigraphs. In these cases, however, the (possibly more than one) edges connecting the same vertices could not be distinguished anymore. Therefore, this definition should only be used for undirected simple graphs. (Contributed by AV, 1-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Edges = (𝑔 ∈ V ↦ ran (2nd ‘𝑔)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uslgrav 25866 | The classes of vertices and edges of an undirected simple graph with loops are sets. (Contributed by Alexander van der Vekens, 20-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USLGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | usgrav 25867 | The classes of vertices and edges of an undirected simple graph without loops are sets. (Contributed by Alexander van der Vekens, 19-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgval 25868 | The edges of a graph. (Contributed by AV, 1-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ 𝑉 → (Edges‘𝐺) = ran (2nd ‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgopval 25869 | The edges of a graph represented as ordered pair. (Contributed by AV, 1-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (Edges‘〈𝑉, 𝐸〉) = ran 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgov 25870 | The edges of a graph, 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 25869. The representation ran 𝐸 for the set of edges is even shorter, though. (Contributed by AV, 2-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉Edges𝐸) = ran 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edguslgra 25871 | The edges of an undirected simple graph with loops. (Contributed by AV, 2-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USLGrph 𝐸 → (𝑉Edges𝐸) = ran 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isuslgra 25872* | The property of being an undirected simple graph with loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉 USLGrph 𝐸 ↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isusgra 25873* | The property of being an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉 USGrph 𝐸 ↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) = 2})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uslgraf 25874* | The edge function of an undirected simple graph with loops is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USLGrph 𝐸 → 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | usgraf 25875* | The edge function of an undirected simple graph without loops is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) = 2}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isusgra0 25876* | The property of being an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 13-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉 USGrph 𝐸 ↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | usgraf0 25877* | The edge function of an undirected simple graph without loops is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 13-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | usgrafun 25878 | The edge function of an undirected simple graph without loops is a function. (Contributed by Alexander van der Vekens, 18-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USGrph 𝐸 → Fun 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | usgraop 25879* | An undirected simple graph without loops represented as ordered pair with a one-to-one edge function. (Contributed by AV, 1-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ USGrph → ∃𝑣∃𝑒(𝐺 = 〈𝑣, 𝑒〉 ∧ 𝑒:dom 𝑒–1-1→{𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | usgrac 25880 | An undirected simple graph represented by a class induces a representation as binary relation. (Contributed by AV, 1-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ USGrph → (1st ‘𝐺) USGrph (2nd ‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgss 25881* | The set of edges of an undirected simple graph without loops is a subset of the set of unordered pairs of vertices. (Contributed by AV, 1-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ USGrph → (Edges‘𝐺) ⊆ {𝑥 ∈ 𝒫 (1st ‘𝐺) ∣ (#‘𝑥) = 2}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edg 25882 | An edge of an undirected simple graph without loops is an unordered pair of vertices. (Contributed by AV, 1-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐺 ∈ USGrph ∧ 𝐸 ∈ (Edges‘𝐺)) → (𝐸 ∈ 𝒫 (1st ‘𝐺) ∧ (#‘𝐸) = 2)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isausgra 25883* | The property of an unordered pair to be an alternatively defined undirected simple graph without loops (defined as a pair (V,E) of a set V (vertex set) and a set of unordered pairs of elements of V (edge set). (Contributed by Alexander van der Vekens, 28-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = {〈𝑣, 𝑒〉 ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2}} ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉𝐺𝐸 ↔ 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ausisusgra 25884* | The equivalence of the definitions of an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 28-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = {〈𝑣, 𝑒〉 ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2}} ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉𝐺𝐸 ↔ 𝑉 USGrph ( I ↾ 𝐸))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ausisusgraedg 25885* | The equivalence of the definitions of an undirected simple graph without loops, expressed with the set of edges. (Contributed by AV, 2-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = {〈𝑣, 𝑒〉 ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2}} ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉𝐺(𝑉Edges𝐸) ↔ 𝑉 USGrph ( I ↾ ran 𝐸))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | usgraedgop 25886 | An edge of an undirected simple graph as second component of an ordered pair. (Contributed by Alexander van der Vekens, 17-Aug-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ dom 𝐸) → ((𝐸‘𝑋) = {𝑀, 𝑁} ↔ 〈𝑋, {𝑀, 𝑁}〉 ∈ 𝐸)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | usgraf1o 25887 | The edge function of an undirected simple graph without loops is a bijective function onto its range. (Contributed by Alexander van der Vekens, 18-Nov-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1-onto→ran 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uslgraf1oedg 25888 | The edge function of an undirected simple graph with loops is a bijective function onto the edges of the graph. (Contributed by AV, 2-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USLGrph 𝐸 → 𝐸:dom 𝐸–1-1-onto→(𝑉Edges𝐸)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | usgraf1 25889 | The edge function of an undirected simple graph without loops is a one to one function. (Contributed by Alexander van der Vekens, 18-Nov-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→ran 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | usgrass 25890 | An edge is a subset of vertices, analogous to umgrass 25848. (Contributed by Alexander van der Vekens, 19-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐹 ∈ dom 𝐸) → (𝐸‘𝐹) ⊆ 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | usgraeq12d 25891 | Equality of simple graphs without loops. (Contributed by Alexander van der Vekens, 11-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝑉 USGrph 𝐸 ↔ 𝑊 USGrph 𝐹)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uslisushgra 25892 | An undirected simple graph with loops is an undirected simple hypergraph. (Contributed by AV, 19-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USLGrph 𝐸 → 𝑉 USHGrph 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uslisumgra 25893 | An undirected simple graph with loops is an undirected multigraph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USLGrph 𝐸 → 𝑉 UMGrph 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | usisuslgra 25894 | An undirected simple graph without loops is an undirected simple graph with loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Proof shortened by Alexander van der Vekens, 20-Mar-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USGrph 𝐸 → 𝑉 USLGrph 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | usisumgra 25895 | An undirected simple graph without loops is an undirected multigraph. (Contributed by Alexander van der Vekens, 20-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USGrph 𝐸 → 𝑉 UMGrph 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | usisuhgra 25896 | An undirected simple graph without loops is an undirected hypergraph. (Contributed by Alexander van der Vekens, 9-Feb-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USGrph 𝐸 → 𝑉 UHGrph 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | elusuhgra 25897 | An undirected simple graph without loops is an undirected hypergraph. (Contributed by AV, 9-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ USGrph → 𝐺 ∈ UHGrph ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | usgrares 25898 | A subgraph of a graph (formed by removing some edges from the original graph) is a graph, analogous to umgrares 25853. (Contributed by Alexander van der Vekens, 10-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 USGrph 𝐸 → 𝑉 USGrph (𝐸 ↾ 𝐴)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | usgra0 25899 | The empty graph, with vertices but no edges, is a graph, analogous to umgra0 25854. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Proof shortened by AV, 25-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑉 ∈ 𝑊 → 𝑉 USGrph ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | usgra0v 25900 | The empty graph with no vertices is a graph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 30-Sep-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (∅ USGrph 𝐸 ↔ 𝐸 = ∅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |