Bridges and bridgeless graphs

DefinitionBridgeless graph#✓fully proved

A simple graph is bridgeless when no edge is a bridge.

def IsBridgeless {V : Type*} (G : SimpleGraph V) : Prop :=
  ∀ e ∈ G.edgeSet, ¬ G.IsBridge e

Used by 5

Used byPetersen coloring conjecture · The edgeless graph is bridgeless · Characterization of bridgeless graphs · Bridgeless from non-bridge edges · Edges of a bridgeless graph are not bridges

TheoremCharacterization of bridgeless graphs#✓fully proved

A simple graph \(G\) is bridgeless if and only if no edge of \(G\) is a bridge.

theorem isBridgeless_iff : G.IsBridgeless ↔ ∀ e ∈ G.edgeSet, ¬ G.IsBridge e

Uses 1

Statement usesBridgeless graph

TheoremBridgeless from non-bridge edges#✓fully proved

If no edge of a simple graph \(G\) is a bridge, then \(G\) is bridgeless.

theorem IsBridgeless.mk (h : ∀ e ∈ G.edgeSet, ¬ G.IsBridge e) : G.IsBridgeless

Uses 1

Statement usesBridgeless graph

TheoremEdges of a bridgeless graph are not bridges#✓fully proved

Every edge of a bridgeless graph is not a bridge.

theorem IsBridgeless.not_isBridge (h : G.IsBridgeless) {e : Sym2 V}
    (he : e ∈ G.edgeSet) : ¬ G.IsBridge e

Uses 1

Statement usesBridgeless graph

TheoremThe edgeless graph is bridgeless#✓fully proved

The edgeless graph on any vertex set is vacuously bridgeless.

theorem isBridgeless_bot (V : Type*) : (⊥ : SimpleGraph V).IsBridgeless

Uses 1

Statement usesBridgeless graph

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.