Helly for connected vertex sets of a finite tree

The proof removes a leaf. Unless one member is that singleton, every member survives removal; two members meeting only at the leaf also contain its neighbour.

def SimpleGraph.prunedSet {N : Type u_1} (S : Set N) (leaf : N) : Set ↑{leaf}ᶜ

Remove a vertex from a set, viewed in the remaining induced graph.

Equations

• SimpleGraph.prunedSet S leaf = {x : ↑{leaf}ᶜ | ↑x ∈ S}

theorem SimpleGraph.leaf_neighbor_mem {N : Type u_1} {T : SimpleGraph N} {leaf neighbour : N} (hunique : ∀ (x : N), T.Adj leaf x → x = neighbour) {S : Set N} (hS : (induce S T).Connected) (hleaf : leaf ∈ S) (hother : ∃ x ∈ S, x ≠ leaf) : neighbour ∈ S

A connected set containing a leaf and another vertex contains its neighbour.

theorem SimpleGraph.connected_prunedSet {N : Type u_1} {T : SimpleGraph N} [Finite N] {leaf neighbour : N} (hadj : T.Adj leaf neighbour) (hunique : ∀ (x : N), T.Adj leaf x → x = neighbour) {S : Set N} (hS : (induce S T).Connected) (hother : ∃ x ∈ S, x ≠ leaf) : (induce (prunedSet S leaf) (induce {leaf}ᶜ T)).Connected

Removing a leaf preserves connectedness of every subtree that has another vertex.

theorem SimpleGraph.prunedSet_inter_nonempty_iff {N : Type u_1} {T : SimpleGraph N} {leaf neighbour : N} (hadj : T.Adj leaf neighbour) (hunique : ∀ (x : N), T.Adj leaf x → x = neighbour) {S R : Set N} (hS : (induce S T).Connected) (hR : (induce R T).Connected) (hSother : ∃ x ∈ S, x ≠ leaf) (hRother : ∃ x ∈ R, x ≠ leaf) : (prunedSet S leaf ∩ prunedSet R leaf).Nonempty ↔ (S ∩ R).Nonempty

Pruning a leaf preserves intersection when both subtrees have another vertex.

theorem SimpleGraph.eq_leaf_of_no_other {N : Type u_1} {S : Set N} {leaf x : N} (hother : ¬∃ y ∈ S, y ≠ leaf) (hx : x ∈ S) : x = leaf

A set with no vertex other than the designated leaf is contained in that singleton.

theorem SimpleGraph.IsTree.prune_subtree_family {N : Type u_1} {T : SimpleGraph N} [Fintype N] [DecidableEq N] (hT : T.IsTree) {leaf neighbour : N} (hadj : T.Adj leaf neighbour) (hunique : ∀ (x : N), T.Adj leaf x → x = neighbour) {I : Type u_2} (F : Finset I) (S : I → Set N) (hc : ∀ i ∈ F, (induce (S i) T).Connected) (hother : ∀ i ∈ F, ∃ x ∈ S i, x ≠ leaf) : Fintype.card ↑{leaf}ᶜ < Fintype.card N ∧ (induce {leaf}ᶜ T).IsTree ∧ (∀ i ∈ F, (induce (prunedSet (S i) leaf) (induce {leaf}ᶜ T)).Connected) ∧ ∀ i ∈ F, ∀ j ∈ F, (prunedSet (S i) leaf ∩ prunedSet (S j) leaf).Nonempty ↔ (S i ∩ S j).Nonempty

The common smaller-host step: pruning preserves the tree, subtrees and intersections.

theorem SimpleGraph.IsTree.finite_subtree_helly {N : Type u_1} {T : SimpleGraph N} [Finite N] (hT : T.IsTree) {I : Type u_2} (F : Finset I) (S : I → Set N) (hconnected : ∀ i ∈ F, (induce (S i) T).Connected) (hinter : ∀ i ∈ F, ∀ j ∈ F, (S i ∩ S j).Nonempty) : ∃ (x : N), ∀ i ∈ F, x ∈ S i

A finite pairwise-intersecting family of nonempty subtrees has a common vertex.