OAI/Analysis/LipschitzFree/BlockObstruction.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Signed finite-rank obstruction on countable bounded metric blocks

  1. abbrev OAI.DiscreteFree.BlockConstruction.Generators line 19
  2. abbrev OAI.DiscreteFree.BlockConstruction.Colors line 20
  3. abbrev OAI.DiscreteFree.BlockConstruction.Ports line 21
  4. abbrev OAI.DiscreteFree.BlockConstruction.Vertices line 22
  5. instance OAI.DiscreteFree.BlockConstruction.(instance at line 24) line 24
  6. instance OAI.DiscreteFree.BlockConstruction.(instance at line 25) line 25
  7. def OAI.DiscreteFree.BlockConstruction.graph line 27
  8. def OAI.DiscreteFree.BlockConstruction.color line 28
  9. abbrev OAI.DiscreteFree.BlockConstruction.Block line 29
  10. def OAI.DiscreteFree.BlockConstruction.baseVertex line 31
  11. def OAI.DiscreteFree.BlockConstruction.base line 33
  12. def OAI.DiscreteFree.BlockConstruction.anchors line 36
  13. theorem OAI.DiscreteFree.BlockConstruction.base_mem line 39
  14. theorem OAI.DiscreteFree.BlockConstruction.attached_mem line 42
  15. theorem OAI.DiscreteFree.BlockConstruction.card_ports line 47
  16. theorem OAI.DiscreteFree.BlockConstruction.nat_card_ports line 50
  17. theorem OAI.DiscreteFree.BlockConstruction.nat_card_colors line 53
  18. theorem OAI.DiscreteFree.BlockConstruction.separation line 57
  19. theorem OAI.DiscreteFree.BlockConstruction.diameter line 60
  20. theorem OAI.DiscreteFree.BlockConstruction.support_colors_bound line 64
  21. theorem OAI.DiscreteFree.BlockConstruction.transition_bound line 70
  22. theorem OAI.DiscreteFree.BlockConstruction.bump_mass line 76
  23. theorem OAI.DiscreteFree.BlockConstruction.finite_support_impossible line 102
  24. theorem OAI.DiscreteFree.BlockConstruction.obstruction line 176
  25. theorem OAI.DiscreteFree.BlockConstruction.original_radius line 188
  26. instance OAI.DiscreteFree.BlockConstruction.infinite_block line 198
  27. theorem OAI.DiscreteFree.blocks_proved line 210