BranchGeometry.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Clique geometry of singleton and doubleton branches and finite clique-minor models.

theorem OAI.HadwigerMatching.connected_card_two_isClique line 11

Source documentation

A connected induced graph on precisely two vertices contains their edge.

theorem connected_card_two_isClique [DecidableEq V] (S : Finset V)
    (hS : S.card = 2) (hc : (G.induce (S : Set V)).Connected) :
    G.IsClique (S : Set V) := by
…

theorem OAI.HadwigerMatching.singleton_vertices_isClique line 40

Source documentation

The vertices of singleton branches form a clique in G.

theorem singleton_vertices_isClique {ι : Type*} (B : ι → Set V)
    (htouch : ∀ i j, i ≠ j → ∃ v ∈ B i, ∃ w ∈ B j, G.Adj v w) :
    G.IsClique {v | ∃ i, B i = {v}} := by
…

theorem OAI.HadwigerMatching.finite_branch_model line 55

Source documentation

On a finite vertex type, clique-minor branches can be represented by finite sets.

theorem finite_branch_model [Fintype V] {t : ℕ}
    (h : LinearListHadwiger.HasCliqueMinor G t) :
    ∃ B : Fin t → Finset V,
      (∀ i, (G.induce (B i : Set V)).Connected) ∧
      (∀ i, (B i).Nonempty) ∧
      Pairwise (fun i j => Disjoint (B i) (B j)) ∧
      (∀ i j, i ≠ j → ∃ v ∈ B i, ∃ w ∈ B j, G.Adj v w) := by
…

Mentions: OAI.LinearListHadwiger.HasCliqueMinor