OAI/Combinatorics/HadwigerMatching/SmallBranches.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Cliques and touching matchings formed by singleton and doubleton branches.

  1. def OAI.HadwigerMatching.singletonVertices line 11
  2. def OAI.HadwigerMatching.twoVertexBranches line 14
  3. theorem OAI.HadwigerMatching.mem_singletonVertices line 17
  4. theorem OAI.HadwigerMatching.mem_twoVertexBranches line 21
  5. theorem OAI.HadwigerMatching.branches_injective line 27

    Source documentation

    Nonemptiness is essential: distinct empty branches would not be injective.

    theorem branches_injective (B : Fin t → Finset V)
    (hne : ∀ i, (B i).Nonempty)
    (hdisj : Pairwise (fun i j => Disjoint (B i) (B j))) :
    Function.Injective B := by
…
  6. theorem OAI.HadwigerMatching.card_singletonVertices line 36
  7. theorem OAI.HadwigerMatching.card_twoVertexBranches line 49
  8. theorem OAI.HadwigerMatching.singleton_branch_eq line 57
  9. theorem OAI.HadwigerMatching.singletonVertices_isClique line 63
  10. theorem OAI.HadwigerMatching.twoVertexBranches_isTouchingMatching line 81
  11. theorem OAI.HadwigerMatching.twoVertexBranches_disjoint_singletonVertices line 100
  12. theorem OAI.HadwigerMatching.singletonVertices_touch_twoVertexBranches line 114