BranchCounting.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Cardinal bounds for pairwise disjoint nonempty branch sets.

def OAI.HadwigerMatching.singletonBranchCount line 16
Source documentation
The number of one-vertex branches.
```
def singletonBranchCount (B : Fin t → Finset V) : ℕ :=
…
```
def OAI.HadwigerMatching.doubletonBranchCount line 20
Source documentation
The number of two-vertex branches.
```
def doubletonBranchCount (B : Fin t → Finset V) : ℕ :=
…
```
theorem OAI.HadwigerMatching.sum_singleton_indicator line 23
theorem OAI.HadwigerMatching.sum_doubleton_indicator line 27

theorem OAI.HadwigerMatching.branch_card_sum_le line 32

Source documentation

Disjoint branch sets occupy at most the ambient finite ground set.

theorem branch_card_sum_le [Fintype V] [DecidableEq V]
    (B : Fin t → Finset V) (hdisj : Pairwise (fun i j => Disjoint (B i) (B j))) :
    (∑ i, (B i).card) ≤ Fintype.card V := by
…

theorem OAI.HadwigerMatching.branch_counting line 42
Source documentation
Every nonempty branch costs at least three, except for the exact deficits of two for a singleton and one for a doubleton.
```
theorem branch_counting [Fintype V] [DecidableEq V]
    (B : Fin t → Finset V)
    (hne : ∀ i, (B i).Nonempty)
    (hdisj : Pairwise (fun i j => Disjoint (B i) (B j))) :
    3 * t ≤ Fintype.card V + 2 * singletonBranchCount B + doubletonBranchCount B := by
…
```
Mentions: OAI.HadwigerMatching.singletonBranchCount, OAI.HadwigerMatching.doubletonBranchCount