Directed graph structures on standard finite sets
Content created by Egbert Rijke, Jonathan Prieto-Cubides, Fredrik Bakke and Vojtěch Štěpančík.
Created on 2022-07-02.
Last modified on 2024-03-23.
module graph-theory.directed-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 univalent-combinatorics.standard-finite-types
Idea
A
directed graph structure¶
on a standard finite set
Fin n
is a binary type-valued relation
Fin n → Fin n → 𝒰.
Definitions
Directed graph structures on standard finite sets
structure-directed-graph-Fin : (l : Level) (n : ℕ) → UU (lsuc l) structure-directed-graph-Fin l n = Fin n → Fin n → UU l
Directed graphs on standard finite sets
Directed-Graph-Fin : (l : Level) → UU (lsuc l) Directed-Graph-Fin l = Σ ℕ (structure-directed-graph-Fin l)
Labeled finite directed graphs on standard finite sets
A
labeled finite directed graph¶
consists of a natural number n
and a map Fin n → Fin n → ℕ
.
Labeled-Finite-Directed-Graph : UU lzero Labeled-Finite-Directed-Graph = Σ ℕ (λ n → Fin n → Fin n → ℕ)
External links
- Directed graph at Mathswitch
- Digraph at Lab
- Directed graph at Lab
- Directed graph on Wikdiata
- Directed graph at Wikipedia
- Directed graph at Wolfram Mathworld
Recent changes
- 2024-03-23. Vojtěch Štěpančík. Enhancements for the Concepts macro (#1093).
- 2024-01-28. Egbert Rijke. Span diagrams (#1007).
- 2023-11-28. Egbert Rijke. Adding more concept tags to graph theory (#953).
- 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).