Complete undirected graphs
Content created by Egbert Rijke, Jonathan Prieto-Cubides, Fredrik Bakke and Vojtěch Štěpančík.
Created on 2022-07-03.
Last modified on 2024-03-23.
module graph-theory.complete-undirected-graphs where
Imports
open import foundation.universe-levels open import graph-theory.complete-multipartite-graphs open import graph-theory.finite-graphs open import univalent-combinatorics.finite-types
Idea
A complete undirected graph¶ is a complete multipartite graph in which every block has exactly one vertex. In other words, it is an undirected graph in which every vertex is connected to every other vertex.
There are many ways of presenting complete undirected graphs. For example, the type of edges in a complete undirected graph is a 2-element subtype of the type of its vertices.
Definition
complete-Undirected-Graph-𝔽 : {l : Level} → 𝔽 l → Undirected-Graph-𝔽 l l complete-Undirected-Graph-𝔽 X = complete-multipartite-Undirected-Graph-𝔽 X (λ x → unit-𝔽)
External links
- Complete graph at Mathswitch
- Complete graph at D3 Graph theory
- Complete graph on Wikidata
- Complete graph on Wikipedia
- Complete graph at Wolfram Mathworld
Recent changes
- 2024-03-23. Vojtěch Štěpančík. Enhancements for the Concepts macro (#1093).
- 2023-11-28. Egbert Rijke. Adding more concept tags to graph theory (#953).
- 2023-10-13. Egbert Rijke. Fix links to wikidata to the recommended links; add concept tags at end of file for testing purposes (#837).
- 2023-10-12. Egbert Rijke. Creating internal and external links in Graph Theory (#832).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).