Undirected graph structures on standard finite sets
Content created by Jonathan Prieto-Cubides, Egbert Rijke and Fredrik Bakke.
Created on 2022-07-02.
Last modified on 2023-11-09.
module graph-theory.undirected-graph-structures-on-standard-finite-sets where
Imports
open import elementary-number-theory.natural-numbers open import foundation.dependent-pair-types open import foundation.universe-levels open import foundation.unordered-pairs open import univalent-combinatorics.standard-finite-types
Definition
Undirected-Graph-Fin : UU (lsuc lzero) Undirected-Graph-Fin = Σ ℕ (λ V → unordered-pair (Fin V) → ℕ)
External links
- Graph at Lab
- Graph on Wikidata
- Graph (discrete mathematics) at Wikipedia
- Graph at Wolfram Mathworld
Recent changes
- 2023-11-09. Fredrik Bakke. Typeset
nlab
as$n$Lab
(#911). - 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-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).