The Helly property of clique trees and the clique number

The bags of a clique tree have the Helly property: every clique of the graph is contained in a single bag. Together with the fact that bags are cliques this identifies the clique number of the graph with the size of the largest bag, and shows that some bag is a maximum clique.

Main results

• SimpleGraph.CliqueTree.exists_subset_bag — every nonempty clique is contained in a bag
• SimpleGraph.CliqueTree.exists_subset_bag' — the same without the nonemptiness assumption, for a nonempty index type
• SimpleGraph.CliqueTree.exists_subset_bag_set — the version for clique sets
• SimpleGraph.CliqueTree.cliqueNum_eq_sup_card_bag — the clique number is the largest bag size
• SimpleGraph.CliqueTree.exists_isMaximumClique_bag — some bag is a maximum clique
• SimpleGraph.IsPEO.cliqueNum_eq_sup_card_peoBag — the same for the bags of a perfect elimination order

theorem SimpleGraph.CliqueTree.top_comparable_of_mem_bag {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {k : ι} {u v : V} (hu : u ∈ T.bag k) (hv : v ∈ T.bag k) : T.IsAncestor (T.top u) (T.top v) ∨ T.IsAncestor (T.top v) (T.top u)

The top nodes of two vertices sharing a bag are comparable.

theorem SimpleGraph.CliqueTree.isAncestor_top_of_rank_le {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {k : ι} {u v : V} (hu : u ∈ T.bag k) (hv : v ∈ T.bag k) (hrank : T.rank (T.top v) ≤ T.rank (T.top u)) : T.IsAncestor (T.top u) (T.top v)

If u and v share a bag and the top node of v has the smaller rank, then the top node of v is an ancestor of the top node of u.

theorem SimpleGraph.CliqueTree.mem_bag_top_of_rank_le {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {k : ι} {u v : V} (hu : u ∈ T.bag k) (hv : v ∈ T.bag k) (hrank : T.rank (T.top v) ≤ T.rank (T.top u)) : v ∈ T.bag (T.top u)

If u and v share a bag and the top node of v has the smaller rank, then v already lies in the top bag of u.

theorem SimpleGraph.CliqueTree.exists_subset_bag {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} (T : G.CliqueTree ι) {K : Finset V} (hK : K.Nonempty) (hKc : G.IsClique ↑K) : ∃ (i : ι), K ⊆ T.bag i

Helly property of the bags. Every nonempty clique of G is contained in a single bag, namely in the top bag of any of its vertices of largest rank.

theorem SimpleGraph.CliqueTree.exists_subset_bag' {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [Nonempty ι] (T : G.CliqueTree ι) {K : Finset V} (hKc : G.IsClique ↑K) : ∃ (i : ι), K ⊆ T.bag i

Helly property of the bags, without a nonemptiness assumption on the clique.

theorem SimpleGraph.CliqueTree.exists_subset_bag_set {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [Finite V] [Nonempty ι] (T : G.CliqueTree ι) {K : Set V} (hKc : G.IsClique K) : ∃ (i : ι), K ⊆ ↑(T.bag i)

Helly property of the bags, for a clique given as a finite set of vertices.

theorem SimpleGraph.CliqueTree.cliqueNum_eq_sup_card_bag {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [Finite V] [Fintype ι] [Nonempty ι] (T : G.CliqueTree ι) : G.cliqueNum = Finset.univ.sup fun (i : ι) => (T.bag i).card

The clique number is the size of the largest bag.

theorem SimpleGraph.CliqueTree.exists_isMaximumClique_bag {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [Finite V] [Finite ι] [Nonempty ι] (T : G.CliqueTree ι) : ∃ (i : ι), G.IsMaximumClique (T.bag i)

Some bag is a maximum clique.

theorem SimpleGraph.IsPEO.cliqueNum_eq_sup_card_peoBag {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] [Nonempty V] {ord : V → ℕ} (h : G.IsPEO ord) : G.cliqueNum = Finset.univ.sup fun (v : V) => (G.peoBag ord v).card

The clique number is the size of the largest bag of a perfect elimination order.