OAI/Combinatorics/ListHadwiger/Density.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LinearListHadwiger.Density.darts line 11
  2. def OAI.LinearListHadwiger.Density.neighbors line 14
  3. lemma OAI.LinearListHadwiger.Density.mem_darts line 16
  4. lemma OAI.LinearListHadwiger.Density.mem_neighbors line 20
  5. lemma OAI.LinearListHadwiger.Density.darts_mono line 23
  6. lemma OAI.LinearListHadwiger.Density.darts_card_le line 28
  7. lemma OAI.LinearListHadwiger.Density.darts_erase line 36
  8. lemma OAI.LinearListHadwiger.Density.darts_separator line 87
  9. theorem OAI.LinearListHadwiger.Density.connectivity_of_density line 106
  10. lemma OAI.LinearListHadwiger.Density.darts_univ line 220
  11. theorem OAI.LinearListHadwiger.Density.edge_density_connectivity line 223