Ear decompositions of simple graphs

An open ear over a subgraph H : G.Subgraph of a simple graph G is a path in G whose two distinct endpoints lie in H, whose internal vertices lie outside H, and whose edges lie outside H (in particular, a single unused edge between two vertices already in H is an open ear). A closed ear over H is a cycle in G meeting H solely at its base vertex; in a simple graph, the unused-edge property follows automatically because every edge of the cycle has at least one endpoint different from the base vertex (SimpleGraph.Ear.closed_edges_notMem_edgeSet).

An ear decomposition d : G.EarDecomposition H is data recording an initial subgraph (either a single vertex or a cycle), a finite sequence of open or closed ears, and the prefix subgraph after each step, ending at H. An ear decomposition is open (SimpleGraph.EarDecomposition.IsOpen) when it starts from a cycle and every ear is open.

This file defines ears, initial subgraphs, and ear decompositions of subgraphs of a simple graph, establishes their extensionality, prefix, and induction API, shows that the initial subgraph and the ears partition the edges of H, and proves without finiteness hypotheses that every ear decomposition builds connected, 2-edge-connected subgraphs (so a decomposition of ⊤ certifies that G is connected and 2-edge-connected). Preservation of 2-vertex-connectivity by open ears and Whitney's open ear characterization are proved in TauCeti.Combinatorics.SimpleGraph.Connectivity.Ear.Open.

Main definitions

• SimpleGraph.EarKind: whether an ear is open or closed.
• SimpleGraph.Ear G H: an open or closed ear in G over H : G.Subgraph.
• SimpleGraph.EarStart G H: witness that H is a singleton subgraph or traced by a cycle.
• SimpleGraph.EarDecomposition G H: a finite ear decomposition in G with final subgraph H.
• SimpleGraph.EarDecomposition.IsOpen: predicate that a decomposition starts from a cycle and adds only open ears.

Main results

• SimpleGraph.Ear.edges_notMem_edgeSet: no edge of an open or closed ear belongs to H.edgeSet.
• SimpleGraph.Ear.lt_adjoin: adjoining an ear strictly enlarges the subgraph.
• SimpleGraph.Ear.isEdgeConnected_two_adjoin: adjoining an ear to a 2-edge-connected subgraph preserves 2-edge-connectivity.
• SimpleGraph.EarDecomposition.ext: an ear decomposition is determined by its length, initial subgraph and witness, and displayed ear walks.
• SimpleGraph.EarDecomposition.subgraphAfter_strictMono: prefix subgraphs grow strictly.
• SimpleGraph.EarDecomposition.mem_edgeSet_initial_or_existsUnique_walkAt: in an ear decomposition of ⊤, every edge outside the initial subgraph belongs to a unique ear.
• SimpleGraph.EarDecomposition.connected, SimpleGraph.EarDecomposition.isEdgeConnected_two: a simple graph admitting an ear decomposition of ⊤ is connected and 2-edge-connected, with no finiteness assumption.

Implementation notes

All projection and predicate bodies (Ear.kind, Ear.toWalk, Ear.toSubgraph, Ear.adjoin, EarStart.IsCycle, EarDecomposition.initial, EarDecomposition.kindAt, EarDecomposition.walkAt, EarDecomposition.IsOpen) remain unexposed, with characteristic @[simp] lemmas proved via := (rfl) so downstream consumers do not rely on definitional unfolding. Only the three length-transforming combinators EarDecomposition.copy, EarDecomposition.snoc, and EarDecomposition.prefix carry @[expose] so dependent Fin indices over .length compute in types.

References

• H. Whitney, Congruent graphs and the connectivity of graphs, Amer. J. Math. 54 (1932), 150–168.
• R. Diestel, Graph Theory, 5th ed., Graduate Texts in Mathematics 173, Springer, 2017, Section 3.1.

inductive SimpleGraph.EarKind : Type

Whether an ear is open (a path between two distinct vertices) or closed (a cycle at one base vertex).

• open : EarKind
• closed : EarKind

@[instance_reducible]

instance SimpleGraph.instDecidableEqEarKind : DecidableEq EarKind

inductive SimpleGraph.Ear {V : Type u} (G : SimpleGraph V) (H : G.Subgraph) : Type u

An ear in G over a subgraph H: either an open ear (a path with distinct endpoints in H, internal vertices outside H, and edges outside H) or a closed ear (a cycle meeting H only at its base vertex). Single-edge open ears are permitted.

• open {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u v : V} (p : G.Walk u v) (hp : p.IsPath) (hu : u ∈ H.verts) (hv : v ∈ H.verts) (huv : u ≠ v) (hint : ∀ w ∈ p.support, w ≠ u → w ≠ v → w ∉ H.verts) (hedge : ∀ e ∈ p.edges, e ∉ H.edgeSet) : G.Ear H
• closed {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u : V} (c : G.Walk u u) (hc : c.IsCycle) (hu : u ∈ H.verts) (hint : ∀ w ∈ c.support, w ≠ u → w ∉ H.verts) : G.Ear H

def SimpleGraph.Ear.kind {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} : G.Ear H → EarKind

Whether an ear is open or closed.

@[simp]

theorem SimpleGraph.Ear.kind_open {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u v : V} (p : G.Walk u v) (hp : p.IsPath) (hu : u ∈ H.verts) (hv : v ∈ H.verts) (huv : u ≠ v) (hint : ∀ w ∈ p.support, w ≠ u → w ≠ v → w ∉ H.verts) (hedge : ∀ e ∈ p.edges, e ∉ H.edgeSet) : («open» p hp hu hv huv hint hedge).kind = EarKind.open

@[simp]

theorem SimpleGraph.Ear.kind_closed {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u : V} (c : G.Walk u u) (hc : c.IsCycle) (hu : u ∈ H.verts) (hint : ∀ w ∈ c.support, w ≠ u → w ∉ H.verts) : (closed c hc hu hint).kind = EarKind.closed

def SimpleGraph.Ear.toWalk {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} : G.Ear H → (u : V) × (v : V) × G.Walk u v

The underlying walk of an ear, packaged with its endpoints.

@[simp]

theorem SimpleGraph.Ear.toWalk_open {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u v : V} (p : G.Walk u v) (hp : p.IsPath) (hu : u ∈ H.verts) (hv : v ∈ H.verts) (huv : u ≠ v) (hint : ∀ w ∈ p.support, w ≠ u → w ≠ v → w ∉ H.verts) (hedge : ∀ e ∈ p.edges, e ∉ H.edgeSet) : («open» p hp hu hv huv hint hedge).toWalk = ⟨u, ⟨v, p⟩⟩

@[simp]

theorem SimpleGraph.Ear.toWalk_closed {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u : V} (c : G.Walk u u) (hc : c.IsCycle) (hu : u ∈ H.verts) (hint : ∀ w ∈ c.support, w ≠ u → w ∉ H.verts) : (closed c hc hu hint).toWalk = ⟨u, ⟨u, c⟩⟩

theorem SimpleGraph.Ear.ext {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {e₁ e₂ : G.Ear H} (h : e₁.toWalk = e₂.toWalk) : e₁ = e₂

Ears over H are determined by their underlying walk; distinctness vs. equality of the walk's endpoints distinguishes open ears from closed ears.

theorem SimpleGraph.Ear.ext_iff {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {e₁ e₂ : G.Ear H} : e₁ = e₂ ↔ e₁.toWalk = e₂.toWalk

def SimpleGraph.Ear.toSubgraph {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} : G.Ear H → G.Subgraph

The subgraph traced by the vertices and edges of an ear.

@[simp]

theorem SimpleGraph.Ear.toSubgraph_open {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u v : V} (p : G.Walk u v) (hp : p.IsPath) (hu : u ∈ H.verts) (hv : v ∈ H.verts) (huv : u ≠ v) (hint : ∀ w ∈ p.support, w ≠ u → w ≠ v → w ∉ H.verts) (hedge : ∀ e ∈ p.edges, e ∉ H.edgeSet) : («open» p hp hu hv huv hint hedge).toSubgraph = p.toSubgraph

@[simp]

theorem SimpleGraph.Ear.toSubgraph_closed {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u : V} (c : G.Walk u u) (hc : c.IsCycle) (hu : u ∈ H.verts) (hint : ∀ w ∈ c.support, w ≠ u → w ∉ H.verts) : (closed c hc hu hint).toSubgraph = c.toSubgraph

theorem SimpleGraph.Ear.toSubgraph_eq_toWalk {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) : e.toSubgraph = e.toWalk.snd.snd.toSubgraph

def SimpleGraph.Ear.adjoin {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) : G.Subgraph

The subgraph obtained by adjoining an ear e to H.

theorem SimpleGraph.Ear.adjoin_def {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) : e.adjoin = H ⊔ e.toSubgraph

@[simp]

theorem SimpleGraph.Ear.verts_adjoin {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) : e.adjoin.verts = H.verts ∪ e.toSubgraph.verts

@[simp]

theorem SimpleGraph.Ear.edgeSet_adjoin {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) : e.adjoin.edgeSet = H.edgeSet ∪ e.toSubgraph.edgeSet

@[simp]

theorem SimpleGraph.Ear.adj_adjoin {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) {u v : V} : e.adjoin.Adj u v ↔ H.Adj u v ∨ e.toSubgraph.Adj u v

theorem SimpleGraph.Ear.le_adjoin {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) : H ≤ e.adjoin

theorem SimpleGraph.Ear.toSubgraph_le_adjoin {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) : e.toSubgraph ≤ e.adjoin

def SimpleGraph.Ear.copy {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph} (e : G.Ear H) (h : H = H') : G.Ear H'

Transport an ear along an equality of base subgraphs without altering its walk data.

@[simp]

theorem SimpleGraph.Ear.copy_rfl {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) : e.copy ⋯ = e

@[simp]

theorem SimpleGraph.Ear.kind_copy {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph} (e : G.Ear H) (h : H = H') : (e.copy h).kind = e.kind

@[simp]

theorem SimpleGraph.Ear.toWalk_copy {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph} (e : G.Ear H) (h : H = H') : (e.copy h).toWalk = e.toWalk

@[simp]

theorem SimpleGraph.Ear.toSubgraph_copy {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph} (e : G.Ear H) (h : H = H') : (e.copy h).toSubgraph = e.toSubgraph

@[simp]

theorem SimpleGraph.Ear.adjoin_copy {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph} (e : G.Ear H) (h : H = H') : (e.copy h).adjoin = H' ⊔ e.toSubgraph

theorem SimpleGraph.Ear.fst_mem_verts {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) : e.toWalk.fst ∈ H.verts

The starting vertex of an ear lies in H.

theorem SimpleGraph.Ear.snd_mem_verts {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) : e.toWalk.snd.fst ∈ H.verts

The ending vertex of an ear lies in H.

theorem SimpleGraph.Ear.isTrail {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) : e.toWalk.snd.snd.IsTrail

Every ear is a trail (its edges are pairwise distinct).

theorem SimpleGraph.Ear.not_nil {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) : ¬e.toWalk.snd.snd.Nil

Every ear has positive length (is not a trivial nil walk).

theorem SimpleGraph.Ear.length_pos {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) : 0 < e.toWalk.snd.snd.length

theorem SimpleGraph.Ear.fst_ne_snd_of_kind_eq_open {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) (he : e.kind = EarKind.open) : e.toWalk.fst ≠ e.toWalk.snd.fst

theorem SimpleGraph.Ear.closed_edges_notMem_edgeSet {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u : V} {c : G.Walk u u} (hint : ∀ w ∈ c.support, w ≠ u → w ∉ H.verts) {x : Sym2 V} (hx : x ∈ c.edges) : x ∉ H.edgeSet

Closed-ear unused-edge property. In a simple graph, a cycle meeting H only at its base vertex uses no edge of H.

theorem SimpleGraph.Ear.edges_notMem_edgeSet {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) {x : Sym2 V} (hx : x ∈ e.toWalk.snd.snd.edges) : x ∉ H.edgeSet

No edge of an open or closed ear belongs to H.edgeSet.

theorem SimpleGraph.Ear.disjoint_edgeSet {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) : Disjoint H.edgeSet e.toSubgraph.edgeSet

theorem SimpleGraph.Ear.lt_adjoin {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (e : G.Ear H) : H < e.adjoin

Adjoining an ear strictly enlarges H.

theorem SimpleGraph.Ear.connected_adjoin {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (hH : H.Preconnected) (e : G.Ear H) : e.adjoin.Connected

Adjoining any open or closed ear to a preconnected subgraph yields a connected subgraph.

theorem SimpleGraph.Ear.isEdgeConnected_two_adjoin {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (hH : H.coe.IsEdgeConnected 2) (e : G.Ear H) : e.adjoin.coe.IsEdgeConnected 2

Adjoining any open or closed ear to a 2-edge-connected subgraph preserves 2-edge-connectivity, with no finiteness assumption.

Initial subgraphs

inductive SimpleGraph.EarStart {V : Type u} (G : SimpleGraph V) : G.Subgraph → Type u

Witness that an initial subgraph H : G.Subgraph of an ear decomposition is either a single vertex or traced by a cycle.

• vertex {V : Type u} {G : SimpleGraph V} (v : V) : G.EarStart (G.singletonSubgraph v)
• cycle {V : Type u} {G : SimpleGraph V} {u : V} (c : G.Walk u u) (hc : c.IsCycle) : G.EarStart c.toSubgraph

def SimpleGraph.EarStart.IsCycle {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} : G.EarStart H → Prop

Whether the initial subgraph is a cycle rather than a single vertex.

@[simp]

theorem SimpleGraph.EarStart.isCycle_vertex {V : Type u} {G : SimpleGraph V} (v : V) : (vertex v).IsCycle ↔ False

@[simp]

theorem SimpleGraph.EarStart.isCycle_cycle {V : Type u} {G : SimpleGraph V} {u : V} (c : G.Walk u u) (hc : c.IsCycle) : (cycle c hc).IsCycle ↔ True

theorem SimpleGraph.EarStart.connected {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} : ∀ (x : G.EarStart H), H.Connected

Every valid initial subgraph is connected.

theorem SimpleGraph.EarStart.isEdgeConnected_two {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} : ∀ (x : G.EarStart H), H.coe.IsEdgeConnected 2

Every valid initial subgraph of an ear decomposition is 2-edge-connected.

Ear decompositions

structure SimpleGraph.EarDecomposition {V : Type u} (G : SimpleGraph V) (H : G.Subgraph) : Type u

A finite ear decomposition in G with final subgraph H, storing the prefix subgraphs, the initial vertex or cycle witness, and the ear added at each step.

• length : ℕ

  The number of ears added after the initial subgraph.

• subgraphAfter : Fin (self.length + 1) → G.Subgraph

  The subgraph built after each prefix; 0 is initial and Fin.last length is H.

• start : G.EarStart (self.subgraphAfter 0)

  Witness that subgraphAfter 0 is a singleton subgraph or traced by a cycle.

• earAt (i : Fin self.length) : G.Ear (self.subgraphAfter i.castSucc)

  The ear added at step i over subgraphAfter i.castSucc.

• subgraphAfter_succ (i : Fin self.length) : self.subgraphAfter i.succ = (self.earAt i).adjoin

  Each successor prefix adjoins its displayed ear.

• subgraphAfter_last : self.subgraphAfter (Fin.last self.length) = H

  The last prefix equals the indexed target subgraph H.

def SimpleGraph.EarDecomposition.initial {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) : G.Subgraph

The initial subgraph (subgraphAfter 0) of an ear decomposition.

@[simp]

theorem SimpleGraph.EarDecomposition.subgraphAfter_zero {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) : d.subgraphAfter 0 = d.initial

def SimpleGraph.EarDecomposition.kindAt {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (i : Fin d.length) : EarKind

The kind (open or closed) of the i-th ear.

theorem SimpleGraph.EarDecomposition.kindAt_def {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (i : Fin d.length) : d.kindAt i = (d.earAt i).kind

def SimpleGraph.EarDecomposition.walkAt {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (i : Fin d.length) : (u : V) × (v : V) × G.Walk u v

The underlying walk (with endpoints) of the i-th ear.

theorem SimpleGraph.EarDecomposition.walkAt_def {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (i : Fin d.length) : d.walkAt i = (d.earAt i).toWalk

theorem SimpleGraph.EarDecomposition.ext {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {d₁ d₂ : G.EarDecomposition H} (hlen : d₁.length = d₂.length) (hinit : d₁.initial = d₂.initial) (hstart : d₁.start ≍ d₂.start) (hwalk : ∀ (i : Fin d₁.length), d₁.walkAt i = d₂.walkAt (Fin.cast hlen i)) : d₁ = d₂

An ear decomposition is determined by its length, initial subgraph and witness, and displayed ear walks; the intermediate prefix subgraphs and ear records are uniquely forced.

theorem SimpleGraph.EarDecomposition.ext_iff {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {d₁ d₂ : G.EarDecomposition H} : d₁ = d₂ ↔ ∃ (hlen : d₁.length = d₂.length), d₁.initial = d₂.initial ∧ d₁.start ≍ d₂.start ∧ ∀ (i : Fin d₁.length), d₁.walkAt i = d₂.walkAt (Fin.cast hlen i)

def SimpleGraph.EarDecomposition.IsOpen {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) : Prop

An ear decomposition is open if it starts from a cycle and every added ear is open.

theorem SimpleGraph.EarDecomposition.isOpen_iff {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) : d.IsOpen ↔ d.start.IsCycle ∧ ∀ (i : Fin d.length), d.kindAt i = EarKind.open

theorem SimpleGraph.EarDecomposition.IsOpen.start_isCycle {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {d : G.EarDecomposition H} (hd : d.IsOpen) : d.start.IsCycle

theorem SimpleGraph.EarDecomposition.IsOpen.kindAt_eq_open {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {d : G.EarDecomposition H} (hd : d.IsOpen) (i : Fin d.length) : d.kindAt i = EarKind.open

theorem SimpleGraph.EarDecomposition.IsOpen.earAt_kind_eq_open {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {d : G.EarDecomposition H} (hd : d.IsOpen) (i : Fin d.length) : (d.earAt i).kind = EarKind.open

def SimpleGraph.EarDecomposition.copy {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph} (d : G.EarDecomposition H) (h : H = H') : G.EarDecomposition H'

Reindex the target subgraph of an ear decomposition along H = H' without changing any data fields.

@[simp]

theorem SimpleGraph.EarDecomposition.copy_rfl {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) : d.copy ⋯ = d

@[simp]

theorem SimpleGraph.EarDecomposition.length_copy {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph} (d : G.EarDecomposition H) (h : H = H') : (d.copy h).length = d.length

@[simp]

theorem SimpleGraph.EarDecomposition.subgraphAfter_copy {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph} (d : G.EarDecomposition H) (h : H = H') : (d.copy h).subgraphAfter = d.subgraphAfter

@[simp]

theorem SimpleGraph.EarDecomposition.initial_copy {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph} (d : G.EarDecomposition H) (h : H = H') : (d.copy h).initial = d.initial

@[simp]

theorem SimpleGraph.EarDecomposition.start_copy {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph} (d : G.EarDecomposition H) (h : H = H') : (d.copy h).start = d.start

@[simp]

theorem SimpleGraph.EarDecomposition.earAt_copy {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph} (d : G.EarDecomposition H) (h : H = H') : (d.copy h).earAt = d.earAt

@[simp]

theorem SimpleGraph.EarDecomposition.walkAt_copy {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph} (d : G.EarDecomposition H) (h : H = H') (i : Fin d.length) : (d.copy h).walkAt i = d.walkAt i

@[simp]

theorem SimpleGraph.EarDecomposition.kindAt_copy {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph} (d : G.EarDecomposition H) (h : H = H') (i : Fin d.length) : (d.copy h).kindAt i = d.kindAt i

@[simp]

theorem SimpleGraph.EarDecomposition.isOpen_copy {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph} (d : G.EarDecomposition H) (h : H = H') : (d.copy h).IsOpen ↔ d.IsOpen

Constructors: vertex, cycle, snoc, and prefix

def SimpleGraph.EarDecomposition.vertex {V : Type u} (G : SimpleGraph V) (v : V) : G.EarDecomposition (G.singletonSubgraph v)

The zero-ear decomposition starting at a single vertex v.

@[simp]

theorem SimpleGraph.EarDecomposition.length_vertex {V : Type u} {G : SimpleGraph V} (v : V) : (vertex G v).length = 0

@[simp]

theorem SimpleGraph.EarDecomposition.subgraphAfter_vertex {V : Type u} {G : SimpleGraph V} (v : V) (k : Fin ((vertex G v).length + 1)) : (vertex G v).subgraphAfter k = G.singletonSubgraph v

@[simp]

theorem SimpleGraph.EarDecomposition.initial_vertex {V : Type u} {G : SimpleGraph V} (v : V) : (vertex G v).initial = G.singletonSubgraph v

@[simp]

theorem SimpleGraph.EarDecomposition.start_vertex {V : Type u} {G : SimpleGraph V} (v : V) : (vertex G v).start = ⋯ ▸ EarStart.vertex v

@[simp]

theorem SimpleGraph.EarDecomposition.not_isOpen_vertex {V : Type u} {G : SimpleGraph V} (v : V) : ¬(vertex G v).IsOpen

def SimpleGraph.EarDecomposition.cycle {V : Type u} {G : SimpleGraph V} {u : V} (c : G.Walk u u) (hc : c.IsCycle) : G.EarDecomposition c.toSubgraph

The zero-ear decomposition starting at a cycle c.

@[simp]

theorem SimpleGraph.EarDecomposition.length_cycle {V : Type u} {G : SimpleGraph V} {u : V} (c : G.Walk u u) (hc : c.IsCycle) : (cycle c hc).length = 0

@[simp]

theorem SimpleGraph.EarDecomposition.subgraphAfter_cycle {V : Type u} {G : SimpleGraph V} {u : V} (c : G.Walk u u) (hc : c.IsCycle) (k : Fin ((cycle c hc).length + 1)) : (cycle c hc).subgraphAfter k = c.toSubgraph

@[simp]

theorem SimpleGraph.EarDecomposition.initial_cycle {V : Type u} {G : SimpleGraph V} {u : V} (c : G.Walk u u) (hc : c.IsCycle) : (cycle c hc).initial = c.toSubgraph

@[simp]

theorem SimpleGraph.EarDecomposition.start_cycle {V : Type u} {G : SimpleGraph V} {u : V} (c : G.Walk u u) (hc : c.IsCycle) : (cycle c hc).start = ⋯ ▸ EarStart.cycle c hc

@[simp]

theorem SimpleGraph.EarDecomposition.isOpen_cycle {V : Type u} {G : SimpleGraph V} {u : V} (c : G.Walk u u) (hc : c.IsCycle) : (cycle c hc).IsOpen

def SimpleGraph.EarDecomposition.snoc {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (e : G.Ear H) : G.EarDecomposition e.adjoin

Append one ear e : G.Ear H to the end of an ear decomposition d : G.EarDecomposition H.

@[simp]

theorem SimpleGraph.EarDecomposition.length_snoc {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (e : G.Ear H) : (d.snoc e).length = d.length + 1

@[simp]

theorem SimpleGraph.EarDecomposition.subgraphAfter_snoc_castSucc {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (e : G.Ear H) (i : Fin (d.length + 1)) : (d.snoc e).subgraphAfter i.castSucc = d.subgraphAfter i

@[simp]

theorem SimpleGraph.EarDecomposition.initial_snoc {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (e : G.Ear H) : (d.snoc e).initial = d.initial

@[simp]

theorem SimpleGraph.EarDecomposition.start_snoc {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (e : G.Ear H) : (d.snoc e).start = ⋯ ▸ d.start

@[simp]

theorem SimpleGraph.EarDecomposition.walkAt_snoc_castSucc {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (e : G.Ear H) (i : Fin d.length) : (d.snoc e).walkAt i.castSucc = d.walkAt i

@[simp]

theorem SimpleGraph.EarDecomposition.walkAt_snoc_last {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (e : G.Ear H) : (d.snoc e).walkAt (Fin.last d.length) = e.toWalk

@[simp]

theorem SimpleGraph.EarDecomposition.kindAt_snoc_castSucc {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (e : G.Ear H) (i : Fin d.length) : (d.snoc e).kindAt i.castSucc = d.kindAt i

@[simp]

theorem SimpleGraph.EarDecomposition.kindAt_snoc_last {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (e : G.Ear H) : (d.snoc e).kindAt (Fin.last d.length) = e.kind

@[simp]

theorem SimpleGraph.EarDecomposition.isOpen_snoc {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (e : G.Ear H) : (d.snoc e).IsOpen ↔ d.IsOpen ∧ e.kind = EarKind.open

def SimpleGraph.EarDecomposition.prefix {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (k : Fin (d.length + 1)) : G.EarDecomposition (d.subgraphAfter k)

The initial segment of d consisting of its first k ears, forming an ear decomposition of d.subgraphAfter k.

@[simp]

theorem SimpleGraph.EarDecomposition.length_prefix {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (k : Fin (d.length + 1)) : (d.prefix k).length = ↑k

@[simp]

theorem SimpleGraph.EarDecomposition.subgraphAfter_prefix {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (k : Fin (d.length + 1)) (j : Fin (↑k + 1)) : (d.prefix k).subgraphAfter j = d.subgraphAfter (Fin.castLE ⋯ j)

@[simp]

theorem SimpleGraph.EarDecomposition.initial_prefix {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (k : Fin (d.length + 1)) : (d.prefix k).initial = d.initial

@[simp]

theorem SimpleGraph.EarDecomposition.start_prefix {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (k : Fin (d.length + 1)) : (d.prefix k).start = d.start

@[simp]

theorem SimpleGraph.EarDecomposition.earAt_prefix {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (k : Fin (d.length + 1)) (j : Fin ↑k) : (d.prefix k).earAt j = d.earAt (Fin.castLE ⋯ j)

@[simp]

theorem SimpleGraph.EarDecomposition.walkAt_prefix {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (k : Fin (d.length + 1)) (j : Fin ↑k) : (d.prefix k).walkAt j = d.walkAt (Fin.castLE ⋯ j)

@[simp]

theorem SimpleGraph.EarDecomposition.kindAt_prefix {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (k : Fin (d.length + 1)) (j : Fin ↑k) : (d.prefix k).kindAt j = d.kindAt (Fin.castLE ⋯ j)

theorem SimpleGraph.EarDecomposition.IsOpen.prefix {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {d : G.EarDecomposition H} (hd : d.IsOpen) (k : Fin (d.length + 1)) : (d.prefix k).IsOpen

Prefix monotonicity and induction

theorem SimpleGraph.EarDecomposition.subgraphAfter_castSucc_lt_succ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (i : Fin d.length) : d.subgraphAfter i.castSucc < d.subgraphAfter i.succ

theorem SimpleGraph.EarDecomposition.subgraphAfter_strictMono {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) : StrictMono d.subgraphAfter

Prefix subgraphs of an ear decomposition are strictly increasing.

theorem SimpleGraph.EarDecomposition.subgraphAfter_mono {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) : Monotone d.subgraphAfter

Prefix subgraphs of an ear decomposition are monotone.

theorem SimpleGraph.EarDecomposition.initial_le_subgraphAfter {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (k : Fin (d.length + 1)) : d.initial ≤ d.subgraphAfter k

theorem SimpleGraph.EarDecomposition.subgraphAfter_le {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (k : Fin (d.length + 1)) : d.subgraphAfter k ≤ H

theorem SimpleGraph.EarDecomposition.initial_le {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) : d.initial ≤ H

theorem SimpleGraph.EarDecomposition.subgraphAfter_induction {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) {P : G.Subgraph → Prop} (h0 : P d.initial) (hstep : ∀ (i : Fin d.length), P (d.subgraphAfter i.castSucc) → P (d.earAt i).adjoin) (k : Fin (d.length + 1)) : P (d.subgraphAfter k)

Induction along the prefix subgraphs of an ear decomposition in construction order.

theorem SimpleGraph.EarDecomposition.final_induction {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) {P : G.Subgraph → Prop} (h0 : P d.initial) (hstep : ∀ (i : Fin d.length), P (d.subgraphAfter i.castSucc) → P (d.earAt i).adjoin) : P H

Induction in construction order proving a property of the final subgraph H.

theorem SimpleGraph.EarDecomposition.prefix_induction {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) {P : ⦃K : G.Subgraph⦄ → G.EarDecomposition K → Prop} (h0 : P (d.prefix 0)) (hstep : ∀ (i : Fin d.length), P (d.prefix i.castSucc) → P (d.prefix i.succ)) (k : Fin (d.length + 1)) : P (d.prefix k)

Induction along the prefix ear decompositions d.prefix k.

Edge partition and coverage

theorem SimpleGraph.EarDecomposition.mem_edgeSet_subgraphAfter_iff {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (k : Fin (d.length + 1)) {x : Sym2 V} : x ∈ (d.subgraphAfter k).edgeSet ↔ x ∈ d.initial.edgeSet ∨ ∃ (i : Fin d.length), i.castSucc < k ∧ x ∈ (d.walkAt i).snd.snd.edges

theorem SimpleGraph.EarDecomposition.mem_edgeSet_iff {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) {x : Sym2 V} : x ∈ H.edgeSet ↔ x ∈ d.initial.edgeSet ∨ ∃ (i : Fin d.length), x ∈ (d.walkAt i).snd.snd.edges

Every edge of H belongs either to d.initial or to one of the added ears.

theorem SimpleGraph.EarDecomposition.notMem_initial_of_mem_walkAt {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (i : Fin d.length) {x : Sym2 V} (hx : x ∈ (d.walkAt i).snd.snd.edges) : x ∉ d.initial.edgeSet

No edge of an added ear belongs to the initial subgraph.

theorem SimpleGraph.EarDecomposition.eq_of_mem_walkAt {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) {i j : Fin d.length} {x : Sym2 V} (hi : x ∈ (d.walkAt i).snd.snd.edges) (hj : x ∈ (d.walkAt j).snd.snd.edges) : i = j

Distinct ears of an ear decomposition share no edges.

theorem SimpleGraph.EarDecomposition.mem_verts_initial_or_walkAt {V : Type u} {G : SimpleGraph V} (d : G.EarDecomposition ⊤) (v : V) : v ∈ d.initial.verts ∨ ∃ (i : Fin d.length), v ∈ (d.walkAt i).snd.snd.support

An ear decomposition of ⊤ covers every vertex of G.

theorem SimpleGraph.EarDecomposition.mem_edgeSet_initial_or_existsUnique_walkAt {V : Type u} {G : SimpleGraph V} (d : G.EarDecomposition ⊤) {x : Sym2 V} (hx : x ∈ G.edgeSet) : x ∈ d.initial.edgeSet ∨ ∃! i : Fin d.length, x ∈ (d.walkAt i).snd.snd.edges

An ear decomposition of ⊤ partitions every edge of G outside d.initial into a unique added ear.

Preservation of connectedness and 2-edge-connectivity

theorem SimpleGraph.EarDecomposition.connected_subgraphAfter {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (k : Fin (d.length + 1)) : (d.subgraphAfter k).Connected

Every prefix subgraph of an ear decomposition is connected.

theorem SimpleGraph.EarDecomposition.connected_final {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) : H.Connected

The final subgraph of an ear decomposition is connected.

theorem SimpleGraph.EarDecomposition.connected {V : Type u} {G : SimpleGraph V} (d : G.EarDecomposition ⊤) : G.Connected

A simple graph with an ear decomposition of ⊤ is connected, with no finiteness assumption.

theorem SimpleGraph.EarDecomposition.isEdgeConnected_two_subgraphAfter {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) (k : Fin (d.length + 1)) : (d.subgraphAfter k).coe.IsEdgeConnected 2

Every prefix subgraph of an ear decomposition is 2-edge-connected.

theorem SimpleGraph.EarDecomposition.isEdgeConnected_two_final {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (d : G.EarDecomposition H) : H.coe.IsEdgeConnected 2

The final subgraph of an ear decomposition is 2-edge-connected.

theorem SimpleGraph.EarDecomposition.isEdgeConnected_two {V : Type u} {G : SimpleGraph V} (d : G.EarDecomposition ⊤) : G.IsEdgeConnected 2

A simple graph with an ear decomposition of ⊤ is 2-edge-connected, with no finiteness assumption.