OAI/Combinatorics/SparsestCut/CellInterface.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniformSparsestCut.CellInterface.floor_locally_constant line 17
  2. lemma OAI.UniformSparsestCut.CellInterface.neighboring_labels line 24
  3. def OAI.UniformSparsestCut.CellInterface.regular line 114
  4. def OAI.UniformSparsestCut.CellInterface.label line 117
  5. def OAI.UniformSparsestCut.CellInterface.LabelVertex line 119
  6. def OAI.UniformSparsestCut.CellInterface.vertex line 122
  7. lemma OAI.UniformSparsestCut.CellInterface.regular_floor_le line 126
  8. lemma OAI.UniformSparsestCut.CellInterface.floor_lt line 132
  9. def OAI.UniformSparsestCut.CellInterface.pattern line 136
  10. def OAI.UniformSparsestCut.CellInterface.weakPattern line 138
  11. lemma OAI.UniformSparsestCut.CellInterface.mem_pattern line 142
  12. lemma OAI.UniformSparsestCut.CellInterface.pattern_labels line 156
  13. def OAI.UniformSparsestCut.CellInterface.extension line 171
  14. lemma OAI.UniformSparsestCut.CellInterface.extension_eq line 179
  15. lemma OAI.UniformSparsestCut.CellInterface.extension_bounded line 195
  16. lemma OAI.UniformSparsestCut.CellInterface.mem_pattern_at line 216
  17. lemma OAI.UniformSparsestCut.CellInterface.mem_weakPattern_at line 235
  18. lemma OAI.UniformSparsestCut.CellInterface.boundary_pattern line 242
  19. lemma OAI.UniformSparsestCut.CellInterface.interface_extension_traces line 263
  20. lemma OAI.UniformSparsestCut.CellInterface.interface_jump_bound line 337