OAI/Combinatorics/CycleDecomposition/UniformLayers.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ErdosGallai.Scale.Layers line 18
  2. theorem OAI.ErdosGallai.Scale.uniform_layers line 29
  3. abbrev OAI.ErdosGallai.Scale.Layers.frontier line 60
  4. abbrev OAI.ErdosGallai.Scale.Layers.scale line 61
  5. abbrev OAI.ErdosGallai.Scale.Layers.mass line 62
  6. abbrev OAI.ErdosGallai.Scale.Layers.pieceMass line 63
  7. lemma OAI.ErdosGallai.Scale.Layers.mass_lower line 65
  8. lemma OAI.ErdosGallai.Scale.Layers.mass_upper line 68
  9. lemma OAI.ErdosGallai.Scale.Layers.mass_two line 80
  10. lemma OAI.ErdosGallai.Scale.Layers.pieceMass_two line 93
  11. lemma OAI.ErdosGallai.Scale.Layers.cycles_bound line 99
  12. lemma OAI.ErdosGallai.Scale.Layers.subset line 110
  13. lemma OAI.ErdosGallai.Scale.Layers.box_subset line 113
  14. lemma OAI.ErdosGallai.Scale.Layers.boundary_order line 117
  15. lemma OAI.ErdosGallai.Scale.Layers.local_mass line 125
  16. lemma OAI.ErdosGallai.Scale.Layers.local_mass_two line 145
  17. lemma OAI.ErdosGallai.Scale.Layers.gap_order line 156
  18. lemma OAI.ErdosGallai.disjoint_subset_mass line 191
  19. theorem OAI.ErdosGallai.uniform_box_cost line 203