BasicMatching.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HadwigerMatching.isTouchingMatching_empty line 14
Source documentation
The empty family is a touching matching.
```
theorem isTouchingMatching_empty (G : SimpleGraph V) :
    IsTouchingMatching G ∅ := by
…
```
Mentions: OAI.HadwigerMatching.IsTouchingMatching
theorem OAI.HadwigerMatching.IsTouchingMatching.sum_card_eq line 19
Source documentation
Every member contributes exactly two vertices.
```
theorem IsTouchingMatching.sum_card_eq {M : Finset (Finset V)}
    (hM : IsTouchingMatching G M) :
    (∑ e ∈ M, e.card) = 2 * M.card := by
…
```
Mentions: OAI.HadwigerMatching.IsTouchingMatching
theorem OAI.HadwigerMatching.IsTouchingMatching.two_mul_card_le line 26
Source documentation
Disjointness bounds twice the number of matching edges by the graph order.
```
theorem IsTouchingMatching.two_mul_card_le [Fintype V]
    {M : Finset (Finset V)} (hM : IsTouchingMatching G M) :
    2 * M.card ≤ Fintype.card V := by
…
```
Mentions: OAI.HadwigerMatching.IsTouchingMatching
theorem OAI.HadwigerMatching.connectedMatchingNumber_bddAbove line 40
Source documentation
Touching matching cardinalities are bounded on a finite vertex type.
```
theorem connectedMatchingNumber_bddAbove [Fintype V] (G : SimpleGraph V) :
    BddAbove {n : ℕ | ∃ M : Finset (Finset V),
      IsTouchingMatching G M ∧ M.card = n} := by
…
```
Mentions: OAI.HadwigerMatching.IsTouchingMatching
theorem OAI.HadwigerMatching.matching_card_le_number line 50
Source documentation
Every touching matching is bounded by the connected matching number.
```
theorem matching_card_le_number [Fintype V] {M : Finset (Finset V)}
    (hM : IsTouchingMatching G M) : M.card ≤ connectedMatchingNumber G := by
…
```
Mentions: OAI.HadwigerMatching.IsTouchingMatching, OAI.HadwigerMatching.connectedMatchingNumber
theorem OAI.HadwigerMatching.exists_matching_card_eq_number line 55
Source documentation
The connected matching number is realized by a touching matching.
```
theorem exists_matching_card_eq_number [Fintype V] (G : SimpleGraph V) :
    ∃ M : Finset (Finset V), IsTouchingMatching G M ∧
      M.card = connectedMatchingNumber G := by
…
```
Mentions: OAI.HadwigerMatching.IsTouchingMatching, OAI.HadwigerMatching.connectedMatchingNumber