OAI/Combinatorics/HadwigerMatching/FinitePairing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerMatching.exists_finite_pairing line 10

   Source documentation

   A finite set admits pairwise disjoint two-element subsets covering all but at most one of its elements, without requiring the ambient type to be finite.

   theorem exists_finite_pairing {V : Type*} (S : Finset V) :
       ∃ P : Finset (Finset V),
         (∀ A ∈ P, A.card = 2 ∧ A ⊆ S) ∧
         (∀ A ∈ P, ∀ B ∈ P, A ≠ B → Disjoint A B) ∧
         2 * P.card ≤ S.card ∧ S.card ≤ 2 * P.card + 1 := by
   …