Connected graphs
Content created by Jonathan Prieto-Cubides, Egbert Rijke and Fredrik Bakke.
Created on 2022-03-16.
Last modified on 2023-11-09.
module graph-theory.connected-undirected-graphs where
Imports
open import foundation.propositional-truncations open import foundation.propositions open import foundation.universe-levels open import graph-theory.undirected-graphs open import graph-theory.walks-undirected-graphs
Idea
An undirected graph is said to be connected if any point can be reached from any point by a walk.
Definition
module _ {l1 l2 : Level} (G : Undirected-Graph l1 l2) where is-connected-Undirected-Graph : UU (l1 ⊔ l2 ⊔ lsuc lzero) is-connected-Undirected-Graph = (x y : vertex-Undirected-Graph G) → type-trunc-Prop (walk-Undirected-Graph G x y)
Properties
The property of being connected for an undirected graph is a proposition
is-prop-is-connected-Undirected-Graph : is-prop is-connected-Undirected-Graph is-prop-is-connected-Undirected-Graph = is-prop-Π (λ _ → is-prop-Π (λ _ → is-prop-type-trunc-Prop))
External links
- Connected graph at Lab
- Connected graph on Wikidata
- Connectivity (graph theory) on Wikipedia
- Connected 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-05-28. Fredrik Bakke. Enforce even indentation and automate some conventions (#635).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).