OAI/Analysis/LipschitzFree/Main.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A countable separated free space with AP and no finite BAP constant

  1. instance OAI.DiscreteFree.MainConstruction.radius_fact line 17
  2. abbrev OAI.DiscreteFree.MainConstruction.Piece line 20
  3. def OAI.DiscreteFree.MainConstruction.pieceBase line 21
  4. abbrev OAI.DiscreteFree.MainConstruction.Space line 22
  5. def OAI.DiscreteFree.MainConstruction.base line 23
  6. theorem OAI.DiscreteFree.MainConstruction.component_separated line 25
  7. theorem OAI.DiscreteFree.MainConstruction.separated line 28
  8. theorem OAI.DiscreteFree.MainConstruction.unbounded line 31
  9. theorem OAI.DiscreteFree.MainConstruction.nonproper line 50
  10. theorem OAI.DiscreteFree.MainConstruction.hasAP line 64
  11. theorem OAI.DiscreteFree.MainConstruction.noBAP line 69
  12. theorem OAI.DiscreteFree.main_proved line 82
  13. theorem OAI.DiscreteFree.source_endpoints line 92

    Distinct definitions of this name: ComparatorChallenges/DiscreteLipschitzFree.lean:156 (same statement text; different proof or body). Qualify references as OAI.DiscreteFree.source_endpoints@path.