Every finite cograph has a cotree

Seinsche's theorem supplies a separated cut in the graph or its complement. Both parts have fewer vertices, so induction gives their cotrees. In the complement case, exchanging union and join completes the representation. The empty graph is included rather than hidden by a nonempty hypothesis.

theorem SimpleGraph.IsCograph.nonempty_cotreeRepresentation {V : Type u_1} [Finite V] {G : SimpleGraph V} (h : G.IsCograph) : Nonempty G.CotreeRepresentation

Every finite cograph has a cotree representation.

theorem SimpleGraph.isCograph_iff_nonempty_cotreeRepresentation {V : Type u_1} [Finite V] (G : SimpleGraph V) : G.IsCograph ↔ Nonempty G.CotreeRepresentation

For finite graphs, cograph membership is exactly representability by a cotree.

noncomputable def SimpleGraph.IsCograph.cotreeRepresentation {V : Type u_1} [Finite V] {G : SimpleGraph V} (h : G.IsCograph) : G.CotreeRepresentation

Choose a cotree for a finite cograph; no claim of a canonical cotree or an executable recognition algorithm is made.

Equations

• h.cotreeRepresentation = Classical.choice ⋯

noncomputable def SimpleGraph.CotreeRepresentation.induce {V : Type u_1} {G : SimpleGraph V} (R : G.CotreeRepresentation) (s : Set V) : (SimpleGraph.induce s G).CotreeRepresentation

An induced restriction of a represented cograph has a cotree too. This interface uses completeness, rather than asserting that its cotree is a particular pruning of the original certificate.

Equations

• R.induce s = ⋯.cotreeRepresentation