OAI/Combinatorics/HadwigerMatching/PairingExtension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerMatching.extend_matching_by_clique_pairs line 10

   Source documentation

   Disjoint pairs from a clique extend a touching matching when every clique vertex is adjacent to a vertex in each existing matching edge.

   theorem extend_matching_by_clique_pairs {V : Type*} [DecidableEq V]
       (G : SimpleGraph V) (E : Finset (Finset V)) (S : Finset V)
       (hE : IsTouchingMatching G E) (hS : G.IsClique (S : Set V))
       (hdisj : ∀ e ∈ E, Disjoint e S)
       (htouch : ∀ v ∈ S, ∀ e ∈ E, ∃ w ∈ e, G.Adj v w) :
       ∃ P : Finset (Finset V), IsTouchingMatching G (E ∪ P) ∧
         (E ∪ P).card = E.card + P.card ∧ S.card ≤ 2 * P.card + 1 := by
   …

   Mentions: OAI.HadwigerMatching.IsTouchingMatching